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.

source
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
source
theorem coheyting.inf_hnot_self {α : Type u_1} [coheyting_algebra α] (a : α) :
a ⊓ ￢a = coheyting.boundary a
source
theorem coheyting.boundary_le {α : Type u_1} [coheyting_algebra α] {a : α} :
coheyting.boundary a ≤ a
source
theorem coheyting.boundary_le_hnot {α : Type u_1} [coheyting_algebra α] {a : α} :
coheyting.boundary a ≤ ￢a
source
@[simp]
theorem coheyting.boundary_bot {α : Type u_1} [coheyting_algebra α] :
coheyting.boundary ⊥ = ⊥
source
@[simp]
theorem coheyting.boundary_top {α : Type u_1} [coheyting_algebra α] :
coheyting.boundary ⊤ = ⊥
source
theorem coheyting.boundary_hnot_le {α : Type u_1} [coheyting_algebra α] (a : α) :
coheyting.boundary (￢a) ≤ coheyting.boundary a
source
@[simp]
theorem coheyting.boundary_hnot_hnot {α : Type u_1} [coheyting_algebra α] (a : α) :
coheyting.boundary (￢￢a) = coheyting.boundary (￢a)
source
@[simp]
theorem coheyting.hnot_boundary {α : Type u_1} [coheyting_algebra α] (a : α) :
￢coheyting.boundary a = ⊤
source
theorem coheyting.boundary_inf {α : Type u_1} [coheyting_algebra α] (a b : α) :
coheyting.boundary (a ⊓ b) = coheyting.boundary a ⊓ b ⊔ a ⊓ coheyting.boundary b

Leibniz rule for the co-Heyting boundary.

source
theorem coheyting.boundary_inf_le {α : Type u_1} [coheyting_algebra α] {a b : α} :
coheyting.boundary (a ⊓ b) ≤ coheyting.boundary a ⊔ coheyting.boundary b
source
theorem coheyting.boundary_sup_le {α : Type u_1} [coheyting_algebra α] {a b : α} :
coheyting.boundary (a ⊔ b) ≤ coheyting.boundary a ⊔ coheyting.boundary b
source
theorem coheyting.boundary_le_boundary_sup_sup_boundary_inf_left {α : Type u_1} [coheyting_algebra α] {a b : α} :
coheyting.boundary a ≤ coheyting.boundary (a ⊔ b) ⊔ coheyting.boundary (a ⊓ b)
source
theorem coheyting.boundary_le_boundary_sup_sup_boundary_inf_right {α : Type u_1} [coheyting_algebra α] {a b : α} :
coheyting.boundary b ≤ coheyting.boundary (a ⊔ b) ⊔ coheyting.boundary (a ⊓ b)
source
theorem coheyting.boundary_sup_sup_boundary_inf {α : Type u_1} [coheyting_algebra α] (a b : α) :
coheyting.boundary (a ⊔ b) ⊔ coheyting.boundary (a ⊓ b) = coheyting.boundary a ⊔ coheyting.boundary b
source
@[simp]
theorem coheyting.boundary_idem {α : Type u_1} [coheyting_algebra α] (a : α) :
coheyting.boundary (coheyting.boundary a) = coheyting.boundary a
source
theorem coheyting.hnot_hnot_sup_boundary {α : Type u_1} [coheyting_algebra α] (a : α) :
￢￢a ⊔ coheyting.boundary a = a
source
theorem coheyting.hnot_eq_top_iff_exists_boundary {α : Type u_1} [coheyting_algebra α] {a : α} :
￢a = ⊤ ↔ ∃ (b : α), coheyting.boundary b = a
source
@[simp]
theorem coheyting.boundary_eq_bot {α : Type u_1} [boolean_algebra α] (a : α) :
coheyting.boundary a = ⊥