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.

source
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
Instances For
    source
    def Heyting.«term∂_» :
    Lean.ParserDescr

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

    Equations
    Instances For
      source
      theorem Coheyting.inf_hnot_self {α : Type u_1} [CoheytingAlgebra α] (a : α) :
      a ⊓ ￢a = Coheyting.boundary a
      source
      theorem Coheyting.boundary_le {α : Type u_1} [CoheytingAlgebra α] {a : α} :
      Coheyting.boundary a ≤ a
      source
      theorem Coheyting.boundary_le_hnot {α : Type u_1} [CoheytingAlgebra α] {a : α} :
      Coheyting.boundary a ≤ ￢a
      source
      @[simp]
      theorem Coheyting.boundary_bot {α : Type u_1} [CoheytingAlgebra α] :
      Coheyting.boundary ⊥ = ⊥
      source
      @[simp]
      theorem Coheyting.boundary_top {α : Type u_1} [CoheytingAlgebra α] :
      Coheyting.boundary ⊤ = ⊥
      source
      theorem Coheyting.boundary_hnot_le {α : Type u_1} [CoheytingAlgebra α] (a : α) :
      Coheyting.boundary (￢a) ≤ Coheyting.boundary a
      source
      @[simp]
      theorem Coheyting.boundary_hnot_hnot {α : Type u_1} [CoheytingAlgebra α] (a : α) :
      Coheyting.boundary (￢￢a) = Coheyting.boundary (￢a)
      source
      @[simp]
      theorem Coheyting.hnot_boundary {α : Type u_1} [CoheytingAlgebra α] (a : α) :
      ￢Coheyting.boundary a = ⊤
      source
      theorem Coheyting.boundary_inf {α : Type u_1} [CoheytingAlgebra α] (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} [CoheytingAlgebra α] {a b : α} :
      Coheyting.boundary (a ⊓ b) ≤ Coheyting.boundary a ⊔ Coheyting.boundary b
      source
      theorem Coheyting.boundary_sup_le {α : Type u_1} [CoheytingAlgebra α] {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} [CoheytingAlgebra α] {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} [CoheytingAlgebra α] {a b : α} :
      Coheyting.boundary b ≤ Coheyting.boundary (a ⊔ b) ⊔ Coheyting.boundary (a ⊓ b)
      source
      theorem Coheyting.boundary_sup_sup_boundary_inf {α : Type u_1} [CoheytingAlgebra α] (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} [CoheytingAlgebra α] (a : α) :
      Coheyting.boundary (Coheyting.boundary a) = Coheyting.boundary a
      source
      theorem Coheyting.hnot_hnot_sup_boundary {α : Type u_1} [CoheytingAlgebra α] (a : α) :
      ￢￢a ⊔ Coheyting.boundary a = a
      source
      theorem Coheyting.hnot_eq_top_iff_exists_boundary {α : Type u_1} [CoheytingAlgebra α] {a : α} :
      ￢a = ⊤ ↔ ∃ (b : α), Coheyting.boundary b = a
      source
      @[simp]
      theorem Coheyting.boundary_eq_bot {α : Type u_1} [BooleanAlgebra α] (a : α) :
      Coheyting.boundary a = ⊥