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} [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

Coheyting.boundary a = a ⊓ ￢a

def Heyting.«term∂_» :

Lean.ParserDescr

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

Equations

Heyting.«term∂_» = Lean.ParserDescr.node `Heyting.term∂_ 120 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "∂ ") (Lean.ParserDescr.cat `term 120))

theorem Coheyting.inf_hnot_self {α : Type u_1} [inst : CoheytingAlgebra α] (a : α) :

a ⊓ ￢a = Coheyting.boundary a

theorem Coheyting.boundary_le {α : Type u_1} [inst : CoheytingAlgebra α] {a : α} :

Coheyting.boundary a ≤ a

theorem Coheyting.boundary_le_hnot {α : Type u_1} [inst : CoheytingAlgebra α] {a : α} :

Coheyting.boundary a ≤ ￢a

@[simp]

theorem Coheyting.boundary_bot {α : Type u_1} [inst : CoheytingAlgebra α] :

Coheyting.boundary ⊥ = ⊥

@[simp]

theorem Coheyting.boundary_top {α : Type u_1} [inst : CoheytingAlgebra α] :

Coheyting.boundary ⊤ = ⊥

theorem Coheyting.boundary_hnot_le {α : Type u_1} [inst : CoheytingAlgebra α] (a : α) :

Coheyting.boundary (￢a) ≤ Coheyting.boundary a

@[simp]

theorem Coheyting.boundary_hnot_hnot {α : Type u_1} [inst : CoheytingAlgebra α] (a : α) :

Coheyting.boundary (￢￢a) = Coheyting.boundary (￢a)

@[simp]

theorem Coheyting.hnot_boundary {α : Type u_1} [inst : CoheytingAlgebra α] (a : α) :

￢Coheyting.boundary a = ⊤

theorem Coheyting.boundary_inf {α : Type u_1} [inst : CoheytingAlgebra α] (a : α) (b : α) :

Coheyting.boundary (a ⊓ b) = Coheyting.boundary a ⊓ b ⊔ a ⊓ Coheyting.boundary b

Leibniz rule for the co-Heyting boundary.

theorem Coheyting.boundary_inf_le {α : Type u_1} [inst : CoheytingAlgebra α] {a : α} {b : α} :

Coheyting.boundary (a ⊓ b) ≤ Coheyting.boundary a ⊔ Coheyting.boundary b

theorem Coheyting.boundary_sup_le {α : Type u_1} [inst : CoheytingAlgebra α] {a : α} {b : α} :

Coheyting.boundary (a ⊔ b) ≤ Coheyting.boundary a ⊔ Coheyting.boundary b

theorem Coheyting.boundary_le_boundary_sup_sup_boundary_inf_left {α : Type u_1} [inst : CoheytingAlgebra α] {a : α} {b : α} :

Coheyting.boundary a ≤ Coheyting.boundary (a ⊔ b) ⊔ Coheyting.boundary (a ⊓ b)

theorem Coheyting.boundary_le_boundary_sup_sup_boundary_inf_right {α : Type u_1} [inst : CoheytingAlgebra α] {a : α} {b : α} :

Coheyting.boundary b ≤ Coheyting.boundary (a ⊔ b) ⊔ Coheyting.boundary (a ⊓ b)

theorem Coheyting.boundary_sup_sup_boundary_inf {α : Type u_1} [inst : CoheytingAlgebra α] (a : α) (b : α) :

Coheyting.boundary (a ⊔ b) ⊔ Coheyting.boundary (a ⊓ b) = Coheyting.boundary a ⊔ Coheyting.boundary b

@[simp]

theorem Coheyting.boundary_idem {α : Type u_1} [inst : CoheytingAlgebra α] (a : α) :

Coheyting.boundary (Coheyting.boundary a) = Coheyting.boundary a

theorem Coheyting.hnot_hnot_sup_boundary {α : Type u_1} [inst : CoheytingAlgebra α] (a : α) :

￢￢a ⊔ Coheyting.boundary a = a

theorem Coheyting.hnot_eq_top_iff_exists_boundary {α : Type u_1} [inst : CoheytingAlgebra α] {a : α} :

￢a = ⊤ ↔ ∃ b, Coheyting.boundary b = a

@[simp]

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

Coheyting.boundary a = ⊥