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} [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} [CoheytingAlgebra α] (a : α) : a ⊓ ￢a = boundary a

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

theorem Coheyting.boundary_le_hnot {α : Type u_1} [CoheytingAlgebra α] {a : α} : boundary a ≤ ￢a

@[simp]

theorem Coheyting.boundary_bot {α : Type u_1} [CoheytingAlgebra α] : boundary ⊥ = ⊥

@[simp]

theorem Coheyting.boundary_top {α : Type u_1} [CoheytingAlgebra α] : boundary ⊤ = ⊥

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

@[simp]

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

@[simp]

theorem Coheyting.hnot_boundary {α : Type u_1} [CoheytingAlgebra α] (a : α) : ￢boundary a = ⊤

theorem Coheyting.boundary_inf {α : Type u_1} [CoheytingAlgebra α] (a b : α) : boundary (a ⊓ b) = boundary a ⊓ b ⊔ a ⊓ boundary b

Leibniz rule for the co-Heyting boundary.

theorem Coheyting.boundary_inf_le {α : Type u_1} [CoheytingAlgebra α] {a b : α} : boundary (a ⊓ b) ≤ boundary a ⊔ boundary b

theorem Coheyting.boundary_sup_le {α : Type u_1} [CoheytingAlgebra α] {a b : α} : boundary (a ⊔ b) ≤ boundary a ⊔ boundary b

theorem Coheyting.boundary_le_boundary_sup_sup_boundary_inf_left {α : Type u_1} [CoheytingAlgebra α] {a b : α} : boundary a ≤ boundary (a ⊔ b) ⊔ boundary (a ⊓ b)

theorem Coheyting.boundary_le_boundary_sup_sup_boundary_inf_right {α : Type u_1} [CoheytingAlgebra α] {a b : α} : boundary b ≤ boundary (a ⊔ b) ⊔ boundary (a ⊓ b)

theorem Coheyting.boundary_sup_sup_boundary_inf {α : Type u_1} [CoheytingAlgebra α] (a b : α) : boundary (a ⊔ b) ⊔ boundary (a ⊓ b) = boundary a ⊔ boundary b

@[simp]

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

theorem Coheyting.hnot_hnot_sup_boundary {α : Type u_1} [CoheytingAlgebra α] (a : α) : ￢￢a ⊔ boundary a = a

theorem Coheyting.hnot_eq_top_iff_exists_boundary {α : Type u_1} [CoheytingAlgebra α] {a : α} : ￢a = ⊤ ↔ ∃ (b : α), boundary b = a

@[simp]

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