mathlib

0ab31714 - feat(order/heyting/boundary): Co-Heyting boundary (#16257)

feat(order/heyting/boundary): Co-Heyting boundary (#16257) Define the boundary of an element in a co-Heyting algebra. This generalizes the topological boundary as an operation on `closeds α`.