# Documentation

Mathlib.Order.Heyting.Boundary

# Co-Heyting boundary #

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
Instances For

The boundary of an element of a co-Heyting algebra.

Equations
Instances For
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 : α) :