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 #

Notation #

∂ a is notation for Coheyting.boundary a in locale Heyting.

def Coheyting.boundary {α : Type u_1} [inst : CoheytingAlgebra α] (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

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

Equations
theorem Coheyting.inf_hnot_self {α : Type u_1} [inst : CoheytingAlgebra α] (a : α) :
theorem Coheyting.boundary_le {α : Type u_1} [inst : CoheytingAlgebra α] {a : α} :
@[simp]
theorem Coheyting.hnot_boundary {α : Type u_1} [inst : CoheytingAlgebra α] (a : α) :
theorem Coheyting.boundary_inf {α : Type u_1} [inst : CoheytingAlgebra α] (a : α) (b : α) :

Leibniz rule for the co-Heyting boundary.

@[simp]
theorem Coheyting.boundary_eq_bot {α : Type u_1} [inst : BooleanAlgebra α] (a : α) :