mathlib3 documentation

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 #

Notation #

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

def coheyting.boundary {α : Type u_1} [coheyting_algebra α] (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} [coheyting_algebra α] (a : α) :
theorem coheyting.boundary_le {α : Type u_1} [coheyting_algebra α] {a : α} :
@[simp]

Leibniz rule for the co-Heyting boundary.

@[simp]
theorem coheyting.boundary_eq_bot {α : Type u_1} [boolean_algebra α] (a : α) :