# mathlib3documentation

order.heyting.boundary

# Co-Heyting boundary #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

The boundary of an element of a co-Heyting algebra is the intersection of its Heyting negation with itself. The boundary in the co-Heyting algebra of closed sets coincides with the topological boundary.

## Main declarations #

• coheyting.boundary: Co-Heyting boundary. coheyting.boundary a = a ⊓ ￢a

## Notation #

∂ a is notation for coheyting.boundary a in locale heyting.

def coheyting.boundary {α : Type u_1} (a : α) :
α

The boundary of an element of a co-Heyting algebra is the intersection of its Heyting negation with itself. Note that this is always ⊥ for a boolean algebra.

Equations
theorem coheyting.inf_hnot_self {α : Type u_1} (a : α) :
a a =
theorem coheyting.boundary_le {α : Type u_1} {a : α} :
theorem coheyting.boundary_le_hnot {α : Type u_1} {a : α} :
@[simp]
theorem coheyting.boundary_bot {α : Type u_1}  :
@[simp]
theorem coheyting.boundary_top {α : Type u_1}  :
theorem coheyting.boundary_hnot_le {α : Type u_1} (a : α) :
@[simp]
theorem coheyting.boundary_hnot_hnot {α : Type u_1} (a : α) :
@[simp]
theorem coheyting.hnot_boundary {α : Type u_1} (a : α) :
theorem coheyting.boundary_inf {α : Type u_1} (a b : α) :

Leibniz rule for the co-Heyting boundary.

theorem coheyting.boundary_inf_le {α : Type u_1} {a b : α} :
theorem coheyting.boundary_sup_le {α : Type u_1} {a b : α} :
@[simp]
theorem coheyting.boundary_idem {α : Type u_1} (a : α) :
theorem coheyting.hnot_hnot_sup_boundary {α : Type u_1} (a : α) :
= a
theorem coheyting.hnot_eq_top_iff_exists_boundary {α : Type u_1} {a : α} :
a = (b : α),
@[simp]
theorem coheyting.boundary_eq_bot {α : Type u_1} (a : α) :