Mathlib.Order.Heyting.Basic

Prod.instHImp instance

[HImp α] [HImp β] : HImp (α × β)

Full source

instance Prod.instHImp [HImp α] [HImp β] : HImp (α × β) :=
  ⟨fun a b => (a.1 ⇨ b.1, a.2 ⇨ b.2)⟩

Componentwise Heyting Implication on Product Types

Informal description

For any two types $\alpha$ and $\beta$ equipped with Heyting implication operations $\Rightarrow$, the product type $\alpha \times \beta$ is also equipped with a Heyting implication operation defined componentwise.

Prod.instHNot instance

[HNot α] [HNot β] : HNot (α × β)

Full source

instance Prod.instHNot [HNot α] [HNot β] : HNot (α × β) :=
  ⟨fun a => (￢a.1, ￢a.2)⟩

Componentwise Heyting Negation on Product Types

Informal description

For any two types $\alpha$ and $\beta$ equipped with a Heyting negation operation $\neg$, the product type $\alpha \times \beta$ also has a Heyting negation operation defined componentwise.

Prod.instSDiff instance

[SDiff α] [SDiff β] : SDiff (α × β)

Full source

instance Prod.instSDiff [SDiff α] [SDiff β] : SDiff (α × β) :=
  ⟨fun a b => (a.1 \ b.1, a.2 \ b.2)⟩

Componentwise Difference Operation on Product Types

Informal description

For any types $\alpha$ and $\beta$ equipped with a difference operation $\setminus$, the product type $\alpha \times \beta$ is also equipped with a difference operation defined componentwise.

Prod.instHasCompl instance

[HasCompl α] [HasCompl β] : HasCompl (α × β)

Full source

instance Prod.instHasCompl [HasCompl α] [HasCompl β] : HasCompl (α × β) :=
  ⟨fun a => (a.1ᶜ, a.2ᶜ)⟩

Componentwise Complement on Product Types

Informal description

For any types $\alpha$ and $\beta$ equipped with a complement operation, the product type $\alpha \times \beta$ also has a complement operation defined componentwise.

fst_himp theorem

[HImp α] [HImp β] (a b : α × β) : (a ⇨ b).1 = a.1 ⇨ b.1

Full source

@[simp]
theorem fst_himp [HImp α] [HImp β] (a b : α × β) : (a ⇨ b).1 = a.1 ⇨ b.1 :=
  rfl

First Component of Heyting Implication in Product Type

Informal description

For any two types $\alpha$ and $\beta$ equipped with Heyting implication operations $\Rightarrow$, and for any elements $a, b$ in the product type $\alpha \times \beta$, the first component of the Heyting implication $a \Rightarrow b$ is equal to the Heyting implication of the first components of $a$ and $b$, i.e., $(a \Rightarrow b)_1 = a_1 \Rightarrow b_1$.

snd_himp theorem

[HImp α] [HImp β] (a b : α × β) : (a ⇨ b).2 = a.2 ⇨ b.2

Full source

@[simp]
theorem snd_himp [HImp α] [HImp β] (a b : α × β) : (a ⇨ b).2 = a.2 ⇨ b.2 :=
  rfl

Second Component of Heyting Implication in Product Type

Informal description

For any two types $\alpha$ and $\beta$ equipped with Heyting implication operations $\Rightarrow$, and for any elements $a, b \in \alpha \times \beta$, the second component of the Heyting implication $a \Rightarrow b$ is equal to the Heyting implication of the second components of $a$ and $b$. That is, $(a \Rightarrow b)_2 = a_2 \Rightarrow b_2$.

fst_hnot theorem

[HNot α] [HNot β] (a : α × β) : (￢a).1 = ￢a.1

Full source

@[simp]
theorem fst_hnot [HNot α] [HNot β] (a : α × β) : (￢a).1 = ￢a.1 :=
  rfl

First Component of Heyting Negation on Product Type

Informal description

For any types $\alpha$ and $\beta$ equipped with a Heyting negation operation $\neg$, and for any element $a = (a_1, a_2) \in \alpha \times \beta$, the first component of the negation $\neg a$ equals the negation of the first component of $a$, i.e., $(\neg a)_1 = \neg a_1$.

snd_hnot theorem

[HNot α] [HNot β] (a : α × β) : (￢a).2 = ￢a.2

Full source

@[simp]
theorem snd_hnot [HNot α] [HNot β] (a : α × β) : (￢a).2 = ￢a.2 :=
  rfl

Second Component of Heyting Negation in Product Type

Informal description

For any types $\alpha$ and $\beta$ equipped with a Heyting negation operation $\neg$, and for any element $a = (a_1, a_2) \in \alpha \times \beta$, the second component of the negation of $a$ equals the negation of the second component of $a$, i.e., $(\neg a)_2 = \neg a_2$.

fst_sdiff theorem

[SDiff α] [SDiff β] (a b : α × β) : (a \ b).1 = a.1 \ b.1

Full source

@[simp]
theorem fst_sdiff [SDiff α] [SDiff β] (a b : α × β) : (a \ b).1 = a.1 \ b.1 :=
  rfl

First Component of Difference in Product Type Equals Difference of First Components

Informal description

For any types $\alpha$ and $\beta$ equipped with a difference operation $\setminus$, and for any elements $a = (a_1, a_2)$ and $b = (b_1, b_2)$ in $\alpha \times \beta$, the first component of the difference $a \setminus b$ equals the difference of their first components, i.e., $(a \setminus b)_1 = a_1 \setminus b_1$.

snd_sdiff theorem

[SDiff α] [SDiff β] (a b : α × β) : (a \ b).2 = a.2 \ b.2

Full source

@[simp]
theorem snd_sdiff [SDiff α] [SDiff β] (a b : α × β) : (a \ b).2 = a.2 \ b.2 :=
  rfl

Second Component of Difference in Product Type Equals Difference of Second Components

Informal description

For any types $\alpha$ and $\beta$ equipped with a difference operation $\setminus$, and for any elements $a = (a_1, a_2)$ and $b = (b_1, b_2)$ in the product type $\alpha \times \beta$, the second component of the difference $a \setminus b$ equals the difference of the second components, i.e., $(a \setminus b)_2 = a_2 \setminus b_2$.

fst_compl theorem

[HasCompl α] [HasCompl β] (a : α × β) : aᶜ.1 = a.1ᶜ

Full source

@[simp]
theorem fst_compl [HasCompl α] [HasCompl β] (a : α × β) : aᶜ.1 = a.1ᶜ :=
  rfl

First Component of Complement in Product Type Equals Complement of First Component

Informal description

For any types $\alpha$ and $\beta$ equipped with a complement operation, and for any element $a = (a_1, a_2) \in \alpha \times \beta$, the first component of the complement of $a$ equals the complement of its first component, i.e., $(a^\complement)_1 = a_1^\complement$.

snd_compl theorem

[HasCompl α] [HasCompl β] (a : α × β) : aᶜ.2 = a.2ᶜ

Full source

@[simp]
theorem snd_compl [HasCompl α] [HasCompl β] (a : α × β) : aᶜ.2 = a.2ᶜ :=
  rfl

Complement Preserves Second Component in Product Types

Informal description

For any types $\alpha$ and $\beta$ equipped with a complement operation, and for any element $a$ in the product type $\alpha \times \beta$, the second component of the complement of $a$ equals the complement of the second component of $a$. That is, $(a^\complement)_2 = (a_2)^\complement$.

Pi.instHImpForall instance

[∀ i, HImp (π i)] : HImp (∀ i, π i)

Full source

instance [∀ i, HImp (π i)] : HImp (∀ i, π i) :=
  ⟨fun a b i => a i ⇨ b i⟩

Pointwise Heyting Implication on Product Types

Informal description

For any family of types $\pi_i$ each equipped with a Heyting implication operation $\Leftarrow$, the product type $\forall i, \pi_i$ is also equipped with a Heyting implication operation, defined pointwise as $(a \Leftarrow b)(i) = a(i) \Leftarrow b(i)$ for all $i$.

Pi.instHNotForall instance

[∀ i, HNot (π i)] : HNot (∀ i, π i)

Full source

instance [∀ i, HNot (π i)] : HNot (∀ i, π i) :=
  ⟨fun a i => ￢a i⟩

Pointwise Heyting Negation on Product Types

Informal description

For any family of types $\pi_i$ each equipped with a Heyting negation operation $\neg$, the product type $\forall i, \pi_i$ inherits a Heyting negation operation defined pointwise as $(\neg a)_i = \neg (a_i)$ for each $a \in \forall i, \pi_i$.

Pi.himp_def theorem

[∀ i, HImp (π i)] (a b : ∀ i, π i) : a ⇨ b = fun i => a i ⇨ b i

Full source

theorem himp_def [∀ i, HImp (π i)] (a b : ∀ i, π i) : a ⇨ b = fun i => a i ⇨ b i :=
  rfl

Pointwise Definition of Heyting Implication on Product Types

Informal description

For any family of types $\pi_i$ indexed by $i \in \iota$ where each $\pi_i$ is equipped with a Heyting implication operation $\Leftarrow$, the Heyting implication on the product type $\forall i, \pi_i$ is defined pointwise as $(a \Leftarrow b)(i) = a(i) \Leftarrow b(i)$ for all $i \in \iota$ and any $a, b \in \forall i, \pi_i$.

Pi.hnot_def theorem

[∀ i, HNot (π i)] (a : ∀ i, π i) : ￢a = fun i => ￢a i

Full source

theorem hnot_def [∀ i, HNot (π i)] (a : ∀ i, π i) : ￢a = fun i => ￢a i :=
  rfl

Pointwise Definition of Heyting Negation in Product Types

Informal description

For any family of types $\pi_i$ indexed by $i$ where each $\pi_i$ is equipped with a Heyting negation operation $\neg$, the negation of an element $a$ in the product type $\forall i, \pi_i$ is defined pointwise as $(\neg a)(i) = \neg (a(i))$ for each index $i$.

Pi.himp_apply theorem

[∀ i, HImp (π i)] (a b : ∀ i, π i) (i : ι) : (a ⇨ b) i = a i ⇨ b i

Full source

@[simp]
theorem himp_apply [∀ i, HImp (π i)] (a b : ∀ i, π i) (i : ι) : (a ⇨ b) i = a i ⇨ b i :=
  rfl

Pointwise Evaluation of Heyting Implication in Product Types

Informal description

For any family of types $\pi_i$ each equipped with a Heyting implication operation $\Rightarrow$, and for any elements $a, b$ in the product type $\forall i, \pi_i$, the Heyting implication $(a \Rightarrow b)$ evaluated at index $i$ is equal to the Heyting implication of $a(i) \Rightarrow b(i)$ in $\pi_i$. That is, $(a \Rightarrow b)(i) = a(i) \Rightarrow b(i)$ for all $i$.

Pi.hnot_apply theorem

[∀ i, HNot (π i)] (a : ∀ i, π i) (i : ι) : (￢a) i = ￢a i

Full source

@[simp]
theorem hnot_apply [∀ i, HNot (π i)] (a : ∀ i, π i) (i : ι) : (￢a) i = ￢a i :=
  rfl

Pointwise Heyting Negation in Product Types: $(\neg a)_i = \neg (a_i)$

Informal description

For any family of types $\pi_i$ each equipped with a Heyting negation operation $\neg$, and for any element $a$ in the product type $\forall i, \pi_i$, the negation of $a$ at index $i$ is equal to the negation of $a_i$, i.e., $(\neg a)_i = \neg (a_i)$ for each $i \in \iota$.

GeneralizedHeytingAlgebra structure

(α : Type*) extends Lattice α, OrderTop α, HImp α

Full source

/-- A generalized Heyting algebra is a lattice with an additional binary operation `⇨` called
Heyting implication such that `(a ⇨ ·)` is right adjoint to `(a ⊓ ·)`.

 This generalizes `HeytingAlgebra` by not requiring a bottom element. -/
class GeneralizedHeytingAlgebra (α : Type*) extends Lattice α, OrderTop α, HImp α where
  /-- `(a ⇨ ·)` is right adjoint to `(a ⊓ ·)` -/
  le_himp_iff (a b c : α) : a ≤ b ⇨ c ↔ a ⊓ b ≤ c

Generalized Heyting Algebra

Informal description

A generalized Heyting algebra is a lattice $\alpha$ equipped with a top element $\top$ and a binary operation $\Rightarrow$ (called Heyting implication) such that for any elements $a, b, c \in \alpha$, the inequality $a \sqcap b \leq c$ holds if and only if $a \leq (b \Rightarrow c)$. This means the operation $(b \Rightarrow \cdot)$ is the right adjoint to $(b \sqcap \cdot)$ in the lattice. Unlike a full Heyting algebra, a generalized Heyting algebra does not require a bottom element.

GeneralizedCoheytingAlgebra structure

(α : Type*) extends Lattice α, OrderBot α, SDiff α

Full source

/-- A generalized co-Heyting algebra is a lattice with an additional binary
difference operation `\` such that `(· \ a)` is left adjoint to `(· ⊔ a)`.

This generalizes `CoheytingAlgebra` by not requiring a top element. -/
class GeneralizedCoheytingAlgebra (α : Type*) extends Lattice α, OrderBot α, SDiff α where
  /-- `(· \ a)` is left adjoint to `(· ⊔ a)` -/
  sdiff_le_iff (a b c : α) : a \ ba \ b ≤ c ↔ a ≤ b ⊔ c

Generalized co-Heyting algebra

Informal description

A generalized co-Heyting algebra is a lattice $\alpha$ with a bottom element $\bot$ and an additional binary operation $\setminus$ (called "difference") such that for any elements $a, b, c \in \alpha$, the inequality $a \setminus b \leq c$ holds if and only if $a \leq b \sqcup c$. This means the operation $(\cdot \setminus a)$ is left adjoint to $(\cdot \sqcup a)$ in the lattice.

HeytingAlgebra structure

(α : Type*) extends GeneralizedHeytingAlgebra α, OrderBot α, HasCompl α

Full source

/-- A Heyting algebra is a bounded lattice with an additional binary operation `⇨` called Heyting
implication such that `(a ⇨ ·)` is right adjoint to `(a ⊓ ·)`. -/
class HeytingAlgebra (α : Type*) extends GeneralizedHeytingAlgebra α, OrderBot α, HasCompl α where
  /-- `aᶜ` is defined as `a ⇨ ⊥` -/
  himp_bot (a : α) : a ⇨ ⊥ = aᶜ

Heyting algebra

Informal description

A Heyting algebra is a bounded lattice $\alpha$ equipped with a binary operation $\Rightarrow$ (called Heyting implication) and a unary operation $\neg$ (called pseudo-complement) such that: 1. The operation $(a \Rightarrow \cdot)$ is the right adjoint to $(a \sqcap \cdot)$, meaning $a \sqcap b \leq c$ if and only if $a \leq (b \Rightarrow c)$ for all $a, b, c \in \alpha$. 2. The pseudo-complement is defined as $\neg a = a \Rightarrow \bot$, where $\bot$ is the bottom element of the lattice. Heyting algebras model intuitionistic logic, where $\sqcap$ represents logical "and", $\sqcup$ represents logical "or", $\Rightarrow$ represents implication, and $\neg$ represents negation.

CoheytingAlgebra structure

(α : Type*) extends GeneralizedCoheytingAlgebra α, OrderTop α, HNot α

Full source

/-- A co-Heyting algebra is a bounded lattice with an additional binary difference operation `\`
such that `(· \ a)` is left adjoint to `(· ⊔ a)`. -/
class CoheytingAlgebra (α : Type*) extends GeneralizedCoheytingAlgebra α, OrderTop α, HNot α where
  /-- `⊤ \ a` is `￢a` -/
  top_sdiff (a : α) : ⊤⊤ \ a = ￢a

Co-Heyting Algebra

Informal description

A co-Heyting algebra is a bounded lattice $\alpha$ equipped with a binary difference operation $\setminus$ and a negation operation $\neg$ (denoted as `￢`), where: 1. The difference operation satisfies the adjunction property: $a \setminus b \leq c$ if and only if $a \leq b \sqcup c$ for all $a, b, c \in \alpha$. 2. The negation is defined as $\neg a = \top \setminus a$. 3. The lattice has both a top element $\top$ and a bottom element $\bot$. This structure is the order-theoretic dual of a Heyting algebra and models a form of co-intuitionistic logic.

BiheytingAlgebra structure

(α : Type*) extends HeytingAlgebra α, SDiff α, HNot α

Full source

/-- A bi-Heyting algebra is a Heyting algebra that is also a co-Heyting algebra. -/
class BiheytingAlgebra (α : Type*) extends HeytingAlgebra α, SDiff α, HNot α where
  /-- `(· \ a)` is left adjoint to `(· ⊔ a)` -/
  sdiff_le_iff (a b c : α) : a \ ba \ b ≤ c ↔ a ≤ b ⊔ c
  /-- `⊤ \ a` is `￢a` -/
  top_sdiff (a : α) : ⊤⊤ \ a = ￢a

Bi-Heyting Algebra

Informal description

A bi-Heyting algebra is a structure that combines both Heyting and co-Heyting algebras. It is a bounded distributive lattice equipped with both an implication operation `⇨` (satisfying `a ≤ b ⇨ c ↔ a ⊓ b ≤ c`) and a difference operation `\` (satisfying `a \ b ≤ c ↔ a ≤ b ⊔ c`), along with pseudo-complement `ᶜ` and negation `￢` operations. In logical terms, this structure models a system that supports both intuitionistic implication and co-implication operations.

HeytingAlgebra.toBoundedOrder instance

[HeytingAlgebra α] : BoundedOrder α

Full source

instance (priority := 100) HeytingAlgebra.toBoundedOrder [HeytingAlgebra α] : BoundedOrder α :=
  { bot_le := ‹HeytingAlgebra α›.bot_le }

Heyting Algebras are Bounded Orders

Informal description

Every Heyting algebra $\alpha$ is a bounded order, meaning it has both a greatest element $\top$ and a least element $\bot$.

CoheytingAlgebra.toBoundedOrder instance

[CoheytingAlgebra α] : BoundedOrder α

Full source

instance (priority := 100) CoheytingAlgebra.toBoundedOrder [CoheytingAlgebra α] : BoundedOrder α :=
  { ‹CoheytingAlgebra α› with }

Co-Heyting Algebras are Bounded Orders

Informal description

Every co-Heyting algebra $\alpha$ is a bounded order, meaning it has both a greatest element $\top$ and a least element $\bot$.

BiheytingAlgebra.toCoheytingAlgebra instance

[BiheytingAlgebra α] : CoheytingAlgebra α

Full source

instance (priority := 100) BiheytingAlgebra.toCoheytingAlgebra [BiheytingAlgebra α] :
    CoheytingAlgebra α :=
  { ‹BiheytingAlgebra α› with }

Bi-Heyting Algebras are Co-Heyting Algebras

Informal description

Every bi-Heyting algebra $\alpha$ is also a co-Heyting algebra. This means that a bi-Heyting algebra, which is a bounded distributive lattice equipped with both Heyting implication $\Rightarrow$ and co-Heyting difference $\setminus$ operations, inherits the structure of a co-Heyting algebra with its difference and negation operations.

HeytingAlgebra.ofHImp abbrev

 [DistribLattice α] [BoundedOrder α] (himp : α → α → α) (le_himp_iff : ∀ a b c, a ≤ himp b c ↔ a ⊓ b ≤ c) :
  HeytingAlgebra α

Full source

/-- Construct a Heyting algebra from the lattice structure and Heyting implication alone. -/
abbrev HeytingAlgebra.ofHImp [DistribLattice α] [BoundedOrder α] (himp : α → α → α)
    (le_himp_iff : ∀ a b c, a ≤ himp b c ↔ a ⊓ b ≤ c) : HeytingAlgebra α :=
  { ‹DistribLattice α›, ‹BoundedOrder α› with
    himp,
    compl := fun a => himp a ⊥,
    le_himp_iff,
    himp_bot := fun _ => rfl }

Construction of Heyting Algebra from Implication Operation

Informal description

Given a distributive lattice $\alpha$ with a bounded order (having top and bottom elements $\top$ and $\bot$), and a binary operation $\Rightarrow : \alpha \to \alpha \to \alpha$ satisfying the adjunction property: \[ a \leq (b \Rightarrow c) \quad \text{if and only if} \quad a \sqcap b \leq c \] for all $a, b, c \in \alpha$, then $\alpha$ can be endowed with the structure of a Heyting algebra where the pseudo-complement is defined as $\neg a = a \Rightarrow \bot$.

HeytingAlgebra.ofCompl abbrev

 [DistribLattice α] [BoundedOrder α] (compl : α → α) (le_himp_iff : ∀ a b c, a ≤ compl b ⊔ c ↔ a ⊓ b ≤ c) :
  HeytingAlgebra α

Full source

/-- Construct a Heyting algebra from the lattice structure and complement operator alone. -/
abbrev HeytingAlgebra.ofCompl [DistribLattice α] [BoundedOrder α] (compl : α → α)
    (le_himp_iff : ∀ a b c, a ≤ compl b ⊔ c ↔ a ⊓ b ≤ c) : HeytingAlgebra α where
  himp := (compl · ⊔ ·)
  compl := compl
  le_himp_iff := le_himp_iff
  himp_bot _ := sup_bot_eq _

Construction of Heyting Algebra from Complement Operation

Informal description

Given a distributive lattice $\alpha$ with a bounded order (having top and bottom elements $\top$ and $\bot$), and a complement operation $\neg : \alpha \to \alpha$ satisfying the adjunction property: \[ a \leq \neg b \sqcup c \quad \text{if and only if} \quad a \sqcap b \leq c \] for all $a, b, c \in \alpha$, then $\alpha$ can be endowed with the structure of a Heyting algebra where the implication operation is defined via the complement.

CoheytingAlgebra.ofSDiff abbrev

 [DistribLattice α] [BoundedOrder α] (sdiff : α → α → α) (sdiff_le_iff : ∀ a b c, sdiff a b ≤ c ↔ a ≤ b ⊔ c) :
  CoheytingAlgebra α

Full source

/-- Construct a co-Heyting algebra from the lattice structure and the difference alone. -/
abbrev CoheytingAlgebra.ofSDiff [DistribLattice α] [BoundedOrder α] (sdiff : α → α → α)
    (sdiff_le_iff : ∀ a b c, sdiff a b ≤ c ↔ a ≤ b ⊔ c) : CoheytingAlgebra α :=
  { ‹DistribLattice α›, ‹BoundedOrder α› with
    sdiff,
    hnot := fun a => sdiff ⊤ a,
    sdiff_le_iff,
    top_sdiff := fun _ => rfl }

Construction of Co-Heyting Algebra from Difference Operation

Informal description

Given a distributive lattice $\alpha$ with a bounded order (having top and bottom elements $\top$ and $\bot$), and a difference operation $\setminus : \alpha \to \alpha \to \alpha$ satisfying the adjunction property: \[ a \setminus b \leq c \quad \text{if and only if} \quad a \leq b \sqcup c \] for all $a, b, c \in \alpha$, then $\alpha$ can be endowed with the structure of a co-Heyting algebra where the negation operation is defined via the difference as $\neg a = \top \setminus a$.

CoheytingAlgebra.ofHNot abbrev

 [DistribLattice α] [BoundedOrder α] (hnot : α → α) (sdiff_le_iff : ∀ a b c, a ⊓ hnot b ≤ c ↔ a ≤ b ⊔ c) :
  CoheytingAlgebra α

Full source

/-- Construct a co-Heyting algebra from the difference and Heyting negation alone. -/
abbrev CoheytingAlgebra.ofHNot [DistribLattice α] [BoundedOrder α] (hnot : α → α)
    (sdiff_le_iff : ∀ a b c, a ⊓ hnot ba ⊓ hnot b ≤ c ↔ a ≤ b ⊔ c) : CoheytingAlgebra α where
  sdiff a b := a ⊓ hnot b
  hnot := hnot
  sdiff_le_iff := sdiff_le_iff
  top_sdiff _ := top_inf_eq _

Construction of Co-Heyting Algebra from Negation Operation

Informal description

Given a distributive lattice $\alpha$ with a bounded order (having top and bottom elements $\top$ and $\bot$), and a negation operation $\neg : \alpha \to \alpha$ satisfying the adjunction property: \[ a \sqcap \neg b \leq c \quad \text{if and only if} \quad a \leq b \sqcup c \] for all $a, b, c \in \alpha$, then $\alpha$ can be endowed with the structure of a co-Heyting algebra where the difference operation is defined via the negation.

le_himp_iff theorem

: a ≤ b ⇨ c ↔ a ⊓ b ≤ c

Full source

/-- `p → q → r ↔ p ∧ q → r` -/
@[simp]
theorem le_himp_iff : a ≤ b ⇨ c ↔ a ⊓ b ≤ c :=
  GeneralizedHeytingAlgebra.le_himp_iff _ _ _

Adjunction Property of Heyting Implication: $a \leq (b \Rightarrow c) \leftrightarrow a \sqcap b \leq c$

Informal description

For any elements $a, b, c$ in a generalized Heyting algebra, the inequality $a \leq (b \Rightarrow c)$ holds if and only if $a \sqcap b \leq c$.

le_himp_iff' theorem

: a ≤ b ⇨ c ↔ b ⊓ a ≤ c

Full source

/-- `p → q → r ↔ q ∧ p → r` -/
theorem le_himp_iff' : a ≤ b ⇨ c ↔ b ⊓ a ≤ c := by rw [le_himp_iff, inf_comm]

Adjunction Property of Heyting Implication (Commuted Version): $a \leq (b \Rightarrow c) \leftrightarrow b \sqcap a \leq c$

Informal description

For any elements $a, b, c$ in a generalized Heyting algebra, the inequality $a \leq (b \Rightarrow c)$ holds if and only if $b \sqcap a \leq c$.

le_himp_comm theorem

: a ≤ b ⇨ c ↔ b ≤ a ⇨ c

Full source

/-- `p → q → r ↔ q → p → r` -/
theorem le_himp_comm : a ≤ b ⇨ c ↔ b ≤ a ⇨ c := by rw [le_himp_iff, le_himp_iff']

Commutativity of Implication Order: $a \leq (b \Rightarrow c) \leftrightarrow b \leq (a \Rightarrow c)$

Informal description

For any elements $a, b, c$ in a generalized Heyting algebra, the inequality $a \leq (b \Rightarrow c)$ holds if and only if $b \leq (a \Rightarrow c)$.

le_himp theorem

: a ≤ b ⇨ a

Full source

/-- `p → q → p` -/
theorem le_himp : a ≤ b ⇨ a :=
  le_himp_iff.2 inf_le_left

Implication Absorption: $a \leq (b \Rightarrow a)$

Informal description

For any elements $a$ and $b$ in a generalized Heyting algebra, the inequality $a \leq (b \Rightarrow a)$ holds. In logical terms, this means that the statement "$b$ implies $a$" is validated whenever $a$ is validated.

le_himp_iff_left theorem

: a ≤ a ⇨ b ↔ a ≤ b

Full source

/-- `p → p → q ↔ p → q` -/
theorem le_himp_iff_left : a ≤ a ⇨ b ↔ a ≤ b := by rw [le_himp_iff, inf_idem]

Left Implication Property: $a \leq (a \Rightarrow b) \leftrightarrow a \leq b$

Informal description

In a generalized Heyting algebra, for any elements $a$ and $b$, the inequality $a \leq (a \Rightarrow b)$ holds if and only if $a \leq b$.

himp_self theorem

: a ⇨ a = ⊤

Full source

/-- `p → p` -/
@[simp]
theorem himp_self : a ⇨ a = ⊤ :=
  top_le_iff.1 <| le_himp_iff.2 inf_le_right

Implication Reflexivity: $a \Rightarrow a = \top$

Informal description

For any element $a$ in a generalized Heyting algebra, the Heyting implication $a \Rightarrow a$ is equal to the top element $\top$.

himp_inf_le theorem

: (a ⇨ b) ⊓ a ≤ b

Full source

/-- `(p → q) ∧ p → q` -/
theorem himp_inf_le : (a ⇨ b) ⊓ a ≤ b :=
  le_himp_iff.1 le_rfl

Implication-Modulated Meet Inequality in Heyting Algebras

Informal description

For any elements $a$ and $b$ in a generalized Heyting algebra, the meet of the Heyting implication $(a \Rightarrow b)$ and $a$ is less than or equal to $b$, i.e., $(a \Rightarrow b) \sqcap a \leq b$.

inf_himp_le theorem

: a ⊓ (a ⇨ b) ≤ b

Full source

/-- `p ∧ (p → q) → q` -/
theorem inf_himp_le : a ⊓ (a ⇨ b) ≤ b := by rw [inf_comm, ← le_himp_iff]

Implication-Modulated Meet Inequality in Heyting Algebras

Informal description

For any elements $a$ and $b$ in a generalized Heyting algebra, the meet of $a$ and the Heyting implication $(a \Rightarrow b)$ is less than or equal to $b$, i.e., $a \sqcap (a \Rightarrow b) \leq b$.

inf_himp theorem

(a b : α) : a ⊓ (a ⇨ b) = a ⊓ b

Full source

/-- `p ∧ (p → q) ↔ p ∧ q` -/
@[simp]
theorem inf_himp (a b : α) : a ⊓ (a ⇨ b) = a ⊓ b :=
  le_antisymm (le_inf inf_le_left <| by rw [inf_comm, ← le_himp_iff]) <| inf_le_inf_left _ le_himp

Meet with Implication Equals Meet: $a \sqcap (a \Rightarrow b) = a \sqcap b$

Informal description

For any elements $a$ and $b$ in a generalized Heyting algebra, the meet of $a$ and the Heyting implication $(a \Rightarrow b)$ equals the meet of $a$ and $b$, i.e., $a \sqcap (a \Rightarrow b) = a \sqcap b$.

himp_inf_self theorem

(a b : α) : (a ⇨ b) ⊓ a = b ⊓ a

Full source

/-- `(p → q) ∧ p ↔ q ∧ p` -/
@[simp]
theorem himp_inf_self (a b : α) : (a ⇨ b) ⊓ a = b ⊓ a := by rw [inf_comm, inf_himp, inf_comm]

Commutativity of Meet with Implication: $(a \Rightarrow b) \sqcap a = b \sqcap a$

Informal description

For any elements $a$ and $b$ in a generalized Heyting algebra, the meet of the Heyting implication $(a \Rightarrow b)$ and $a$ equals the meet of $b$ and $a$, i.e., $(a \Rightarrow b) \sqcap a = b \sqcap a$.

himp_eq_top_iff theorem

: a ⇨ b = ⊤ ↔ a ≤ b

Full source

/-- The **deduction theorem** in the Heyting algebra model of intuitionistic logic:
an implication holds iff the conclusion follows from the hypothesis. -/
@[simp]
theorem himp_eq_top_iff : a ⇨ ba ⇨ b = ⊤ ↔ a ≤ b := by rw [← top_le_iff, le_himp_iff, top_inf_eq]

Equivalence of Implication to Top and Order Relation: $a \Rightarrow b = \top \leftrightarrow a \leq b$

Informal description

In a generalized Heyting algebra, the Heyting implication $a \Rightarrow b$ equals the top element $\top$ if and only if $a$ is less than or equal to $b$, i.e., $a \Rightarrow b = \top \leftrightarrow a \leq b$.

himp_top theorem

: a ⇨ ⊤ = ⊤

Full source

/-- `p → true`, `true → p ↔ p` -/
@[simp]
theorem himp_top : a ⇨ ⊤ = ⊤ :=
  himp_eq_top_iff.2 le_top

Implication to Top is Top: $a \Rightarrow \top = \top$

Informal description

In a generalized Heyting algebra, for any element $a$, the Heyting implication $a \Rightarrow \top$ equals the top element $\top$, i.e., $a \Rightarrow \top = \top$.

top_himp theorem

: ⊤ ⇨ a = a

Full source

@[simp]
theorem top_himp : ⊤⊤ ⇨ a = a :=
  eq_of_forall_le_iff fun b => by rw [le_himp_iff, inf_top_eq]

Top Element Implication Identity: $\top \Rightarrow a = a$

Informal description

In a generalized Heyting algebra, the Heyting implication of the top element $\top$ and any element $a$ is equal to $a$, i.e., $\top \Rightarrow a = a$.

himp_himp theorem

(a b c : α) : a ⇨ b ⇨ c = a ⊓ b ⇨ c

Full source

/-- `p → q → r ↔ p ∧ q → r` -/
theorem himp_himp (a b c : α) : a ⇨ b ⇨ c = a ⊓ ba ⊓ b ⇨ c :=
  eq_of_forall_le_iff fun d => by simp_rw [le_himp_iff, inf_assoc]

Currying Property of Heyting Implication

Informal description

In a generalized Heyting algebra $\alpha$, for any elements $a, b, c \in \alpha$, the Heyting implication satisfies the identity: $$(a \Rightarrow (b \Rightarrow c)) = ((a \sqcap b) \Rightarrow c)$$

himp_le_himp_himp_himp theorem

: b ⇨ c ≤ (a ⇨ b) ⇨ a ⇨ c

Full source

/-- `(q → r) → (p → q) → q → r` -/
theorem himp_le_himp_himp_himp : b ⇨ c ≤ (a ⇨ b) ⇨ a ⇨ c := by
  rw [le_himp_iff, le_himp_iff, inf_assoc, himp_inf_self, ← inf_assoc, himp_inf_self, inf_assoc]
  exact inf_le_left

Monotonicity of Heyting Implication: $(b \Rightarrow c) \leq ((a \Rightarrow b) \Rightarrow (a \Rightarrow c))$

Informal description

In a generalized Heyting algebra, for any elements $a, b, c$, the Heyting implication satisfies the inequality: $$(b \Rightarrow c) \leq ((a \Rightarrow b) \Rightarrow (a \Rightarrow c))$$

himp_inf_himp_inf_le theorem

: (b ⇨ c) ⊓ (a ⇨ b) ⊓ a ≤ c

Full source

@[simp]
theorem himp_inf_himp_inf_le : (b ⇨ c) ⊓ (a ⇨ b)(b ⇨ c) ⊓ (a ⇨ b) ⊓ a ≤ c := by
  simpa using @himp_le_himp_himp_himp

Implication Composition Inequality in Heyting Algebras: $(b \Rightarrow c) \sqcap (a \Rightarrow b) \sqcap a \leq c$

Informal description

In a generalized Heyting algebra, for any elements $a, b, c$, the following inequality holds: $$(b \Rightarrow c) \sqcap (a \Rightarrow b) \sqcap a \leq c.$$

himp_left_comm theorem

(a b c : α) : a ⇨ b ⇨ c = b ⇨ a ⇨ c

Full source

/-- `p → q → r ↔ q → p → r` -/
theorem himp_left_comm (a b c : α) : a ⇨ b ⇨ c = b ⇨ a ⇨ c := by simp_rw [himp_himp, inf_comm]

Left Commutativity of Heyting Implication

Informal description

In a generalized Heyting algebra $\alpha$, for any elements $a, b, c \in \alpha$, the Heyting implication satisfies the following commutative property: $$(a \Rightarrow (b \Rightarrow c)) = (b \Rightarrow (a \Rightarrow c))$$

himp_idem theorem

: b ⇨ b ⇨ a = b ⇨ a

Full source

@[simp]
theorem himp_idem : b ⇨ b ⇨ a = b ⇨ a := by rw [himp_himp, inf_idem]

Idempotence of Heyting Implication: $(b \Rightarrow (b \Rightarrow a)) = (b \Rightarrow a)$

Informal description

In a generalized Heyting algebra $\alpha$, for any elements $a, b \in \alpha$, the Heyting implication satisfies the idempotence property: $$(b \Rightarrow (b \Rightarrow a)) = (b \Rightarrow a).$$

himp_inf_distrib theorem

(a b c : α) : a ⇨ b ⊓ c = (a ⇨ b) ⊓ (a ⇨ c)

Full source

theorem himp_inf_distrib (a b c : α) : a ⇨ b ⊓ c = (a ⇨ b) ⊓ (a ⇨ c) :=
  eq_of_forall_le_iff fun d => by simp_rw [le_himp_iff, le_inf_iff, le_himp_iff]

Distributivity of Implication over Meet in Heyting Algebra

Informal description

In a generalized Heyting algebra $\alpha$, for any elements $a, b, c \in \alpha$, the Heyting implication satisfies the following distributive property: \[ a \Rightarrow (b \sqcap c) = (a \Rightarrow b) \sqcap (a \Rightarrow c). \] This means that implication distributes over meet (infimum) in the second argument.

sup_himp_distrib theorem

(a b c : α) : a ⊔ b ⇨ c = (a ⇨ c) ⊓ (b ⇨ c)

Full source

theorem sup_himp_distrib (a b c : α) : a ⊔ ba ⊔ b ⇨ c = (a ⇨ c) ⊓ (b ⇨ c) :=
  eq_of_forall_le_iff fun d => by
    rw [le_inf_iff, le_himp_comm, sup_le_iff]
    simp_rw [le_himp_comm]

Distributivity of Implication over Join in Heyting Algebra: $(a \sqcup b) \Rightarrow c = (a \Rightarrow c) \sqcap (b \Rightarrow c)$

Informal description

For any elements $a, b, c$ in a generalized Heyting algebra $\alpha$, the Heyting implication satisfies: $$(a \sqcup b) \Rightarrow c = (a \Rightarrow c) \sqcap (b \Rightarrow c).$$ This shows that implication distributes over join (supremum) in the first argument.

himp_le_himp_left theorem

(h : a ≤ b) : c ⇨ a ≤ c ⇨ b

Full source

theorem himp_le_himp_left (h : a ≤ b) : c ⇨ a ≤ c ⇨ b :=
  le_himp_iff.2 <| himp_inf_le.trans h

Monotonicity of Heyting Implication in the Consequent: $a \leq b \implies (c \Rightarrow a) \leq (c \Rightarrow b)$

Informal description

In a generalized Heyting algebra, if $a \leq b$, then for any element $c$, the Heyting implication satisfies $c \Rightarrow a \leq c \Rightarrow b$.

himp_le_himp_right theorem

(h : a ≤ b) : b ⇨ c ≤ a ⇨ c

Full source

theorem himp_le_himp_right (h : a ≤ b) : b ⇨ c ≤ a ⇨ c :=
  le_himp_iff.2 <| (inf_le_inf_left _ h).trans himp_inf_le

Monotonicity of Heyting Implication in the Antecedent: $(a \leq b) \to (b \Rightarrow c) \leq (a \Rightarrow c)$

Informal description

In a generalized Heyting algebra, if $a \leq b$, then the Heyting implication satisfies $(b \Rightarrow c) \leq (a \Rightarrow c)$ for any element $c$.

himp_le_himp theorem

(hab : a ≤ b) (hcd : c ≤ d) : b ⇨ c ≤ a ⇨ d

Full source

theorem himp_le_himp (hab : a ≤ b) (hcd : c ≤ d) : b ⇨ c ≤ a ⇨ d :=
  (himp_le_himp_right hab).trans <| himp_le_himp_left hcd

Monotonicity of Heyting Implication in Both Arguments: $(a \leq b) \land (c \leq d) \to (b \Rightarrow c) \leq (a \Rightarrow d)$

Informal description

In a generalized Heyting algebra, if $a \leq b$ and $c \leq d$, then the Heyting implication satisfies $(b \Rightarrow c) \leq (a \Rightarrow d)$.

sup_himp_self_left theorem

(a b : α) : a ⊔ b ⇨ a = b ⇨ a

Full source

@[simp]
theorem sup_himp_self_left (a b : α) : a ⊔ ba ⊔ b ⇨ a = b ⇨ a := by
  rw [sup_himp_distrib, himp_self, top_inf_eq]

Implication from Join to Left Component: $(a \sqcup b) \Rightarrow a = b \Rightarrow a$

Informal description

For any elements $a$ and $b$ in a generalized Heyting algebra, the Heyting implication satisfies: $$(a \sqcup b) \Rightarrow a = b \Rightarrow a.$$

sup_himp_self_right theorem

(a b : α) : a ⊔ b ⇨ b = a ⇨ b

Full source

@[simp]
theorem sup_himp_self_right (a b : α) : a ⊔ ba ⊔ b ⇨ b = a ⇨ b := by
  rw [sup_himp_distrib, himp_self, inf_top_eq]

Simplification of Implication over Join: $(a \sqcup b) \Rightarrow b = a \Rightarrow b$

Informal description

In a generalized Heyting algebra $\alpha$, for any elements $a$ and $b$, the Heyting implication satisfies: $$(a \sqcup b) \Rightarrow b = a \Rightarrow b.$$ This shows that the implication of a join with $b$ in the first argument and $b$ in the second argument simplifies to the implication of $a$ and $b$.

Codisjoint.himp_eq_right theorem

(h : Codisjoint a b) : b ⇨ a = a

Full source

theorem Codisjoint.himp_eq_right (h : Codisjoint a b) : b ⇨ a = a := by
  conv_rhs => rw [← @top_himp _ _ a]
  rw [← h.eq_top, sup_himp_self_left]

Heyting Implication Identity for Codisjoint Elements: $b \Rightarrow a = a$ when $a \sqcup b = \top$

Informal description

In a generalized Heyting algebra, if two elements $a$ and $b$ are codisjoint (i.e., $a \sqcup b = \top$), then the Heyting implication $b \Rightarrow a$ is equal to $a$.

Codisjoint.himp_eq_left theorem

(h : Codisjoint a b) : a ⇨ b = b

Full source

theorem Codisjoint.himp_eq_left (h : Codisjoint a b) : a ⇨ b = b :=
  h.symm.himp_eq_right

Heyting Implication Identity for Codisjoint Elements: $a \Rightarrow b = b$ when $a \sqcup b = \top$

Informal description

In a generalized Heyting algebra, if two elements $a$ and $b$ are codisjoint (i.e., $a \sqcup b = \top$), then the Heyting implication $a \Rightarrow b$ is equal to $b$.

Codisjoint.himp_inf_cancel_right theorem

(h : Codisjoint a b) : a ⇨ a ⊓ b = b

Full source

theorem Codisjoint.himp_inf_cancel_right (h : Codisjoint a b) : a ⇨ a ⊓ b = b := by
  rw [himp_inf_distrib, himp_self, top_inf_eq, h.himp_eq_left]

Heyting Implication Cancellation for Codisjoint Elements: $a \Rightarrow (a \sqcap b) = b$ when $a \sqcup b = \top$

Informal description

In a generalized Heyting algebra, if two elements $a$ and $b$ are codisjoint (i.e., $a \sqcup b = \top$), then the Heyting implication $a \Rightarrow (a \sqcap b)$ equals $b$.

Codisjoint.himp_inf_cancel_left theorem

(h : Codisjoint a b) : b ⇨ a ⊓ b = a

Full source

theorem Codisjoint.himp_inf_cancel_left (h : Codisjoint a b) : b ⇨ a ⊓ b = a := by
  rw [himp_inf_distrib, himp_self, inf_top_eq, h.himp_eq_right]

Heyting Implication Cancellation for Codisjoint Elements: $b \Rightarrow (a \sqcap b) = a$ when $a \sqcup b = \top$

Informal description

In a generalized Heyting algebra, if two elements $a$ and $b$ are codisjoint (i.e., $a \sqcup b = \top$), then the Heyting implication $b \Rightarrow (a \sqcap b)$ equals $a$.

Codisjoint.himp_le_of_right_le theorem

(hac : Codisjoint a c) (hba : b ≤ a) : c ⇨ b ≤ a

Full source

/-- See `himp_le` for a stronger version in Boolean algebras. -/
theorem Codisjoint.himp_le_of_right_le (hac : Codisjoint a c) (hba : b ≤ a) : c ⇨ b ≤ a :=
  (himp_le_himp_left hba).trans_eq hac.himp_eq_right

Heyting Implication Bound for Codisjoint Elements: $a \sqcup c = \top \land b \leq a \implies (c \Rightarrow b) \leq a$

Informal description

In a generalized Heyting algebra, if elements $a$ and $c$ are codisjoint (i.e., $a \sqcup c = \top$) and $b \leq a$, then the Heyting implication $c \Rightarrow b$ is less than or equal to $a$.

le_himp_himp theorem

: a ≤ (a ⇨ b) ⇨ b

Full source

theorem le_himp_himp : a ≤ (a ⇨ b) ⇨ b :=
  le_himp_iff.2 inf_himp_le

Double Implication Lower Bound: $a \leq ((a \Rightarrow b) \Rightarrow b)$

Informal description

In a generalized Heyting algebra, for any elements $a$ and $b$, the inequality $a \leq ((a \Rightarrow b) \Rightarrow b)$ holds.

himp_eq_himp_iff theorem

: b ⇨ a = a ⇨ b ↔ a = b

Full source

@[simp] lemma himp_eq_himp_iff : b ⇨ ab ⇨ a = a ⇨ b ↔ a = b := by simp [le_antisymm_iff]

Equality of Symmetric Heyting Implications

Informal description

In a generalized Heyting algebra $\alpha$, for any elements $a, b \in \alpha$, the Heyting implications satisfy $b \Rightarrow a = a \Rightarrow b$ if and only if $a = b$.

himp_ne_himp_iff theorem

: b ⇨ a ≠ a ⇨ b ↔ a ≠ b

Full source

lemma himp_ne_himp_iff : b ⇨ ab ⇨ a ≠ a ⇨ bb ⇨ a ≠ a ⇨ b ↔ a ≠ b := himp_eq_himp_iff.not

Inequality of Symmetric Heyting Implications

Informal description

In a generalized Heyting algebra $\alpha$, for any elements $a, b \in \alpha$, the Heyting implications satisfy $b \Rightarrow a \neq a \Rightarrow b$ if and only if $a \neq b$.

himp_triangle theorem

(a b c : α) : (a ⇨ b) ⊓ (b ⇨ c) ≤ a ⇨ c

Full source

theorem himp_triangle (a b c : α) : (a ⇨ b) ⊓ (b ⇨ c) ≤ a ⇨ c := by
  rw [le_himp_iff, inf_right_comm, ← le_himp_iff]
  exact himp_inf_le.trans le_himp_himp

Triangle Inequality for Heyting Implications: $(a \Rightarrow b) \sqcap (b \Rightarrow c) \leq (a \Rightarrow c)$

Informal description

In a generalized Heyting algebra $\alpha$, for any elements $a, b, c \in \alpha$, the meet of the Heyting implications $(a \Rightarrow b)$ and $(b \Rightarrow c)$ is less than or equal to $(a \Rightarrow c)$, i.e., $(a \Rightarrow b) \sqcap (b \Rightarrow c) \leq (a \Rightarrow c)$.

himp_inf_himp_cancel theorem

(hba : b ≤ a) (hcb : c ≤ b) : (a ⇨ b) ⊓ (b ⇨ c) = a ⇨ c

Full source

theorem himp_inf_himp_cancel (hba : b ≤ a) (hcb : c ≤ b) : (a ⇨ b) ⊓ (b ⇨ c) = a ⇨ c :=
  (himp_triangle _ _ _).antisymm <| le_inf (himp_le_himp_left hcb) (himp_le_himp_right hba)

Cancellation Law for Heyting Implications: $(a \Rightarrow b) \sqcap (b \Rightarrow c) = a \Rightarrow c$ under $b \leq a$ and $c \leq b$

Informal description

In a generalized Heyting algebra, if $b \leq a$ and $c \leq b$, then the meet of the Heyting implications $(a \Rightarrow b)$ and $(b \Rightarrow c)$ equals $(a \Rightarrow c)$, i.e., $(a \Rightarrow b) \sqcap (b \Rightarrow c) = a \Rightarrow c$.

gc_inf_himp theorem

: GaloisConnection (a ⊓ ·) (a ⇨ ·)

Full source

theorem gc_inf_himp : GaloisConnection (a ⊓ ·) (a ⇨ ·) :=
  fun _ _ ↦ Iff.symm le_himp_iff'

Galois Connection Between Meet and Implication in Heyting Algebras

Informal description

For any element $a$ in a generalized Heyting algebra, the operation $(a \sqcap \cdot)$ forms a Galois connection with the Heyting implication operation $(a \Rightarrow \cdot)$. That is, for any elements $b$ and $c$ in the algebra, we have $a \sqcap b \leq c$ if and only if $b \leq (a \Rightarrow c)$.

GeneralizedHeytingAlgebra.toDistribLattice instance

: DistribLattice α

Full source

instance (priority := 100) GeneralizedHeytingAlgebra.toDistribLattice : DistribLattice α :=
  DistribLattice.ofInfSupLe fun a b c => by
    simp_rw [inf_comm a, ← le_himp_iff, sup_le_iff, le_himp_iff, ← sup_le_iff]; rfl

Generalized Heyting Algebras are Distributive Lattices

Informal description

Every generalized Heyting algebra $\alpha$ is a distributive lattice.

OrderDual.instGeneralizedCoheytingAlgebra instance

: GeneralizedCoheytingAlgebra αᵒᵈ

Full source

instance OrderDual.instGeneralizedCoheytingAlgebra : GeneralizedCoheytingAlgebra αᵒᵈ where
  sdiff a b := toDual (ofDualofDual b ⇨ ofDual a)
  sdiff_le_iff a b c := by rw [sup_comm]; exact le_himp_iff

Order Dual of a Generalized Heyting Algebra is a Generalized Co-Heyting Algebra

Informal description

For any generalized Heyting algebra $\alpha$, the order dual $\alpha^{\text{op}}$ is a generalized co-Heyting algebra.

Prod.instGeneralizedHeytingAlgebra instance

[GeneralizedHeytingAlgebra β] : GeneralizedHeytingAlgebra (α × β)

Full source

instance Prod.instGeneralizedHeytingAlgebra [GeneralizedHeytingAlgebra β] :
    GeneralizedHeytingAlgebra (α × β) where
  le_himp_iff _ _ _ := and_congr le_himp_iff le_himp_iff

Generalized Heyting Algebra Structure on Product Types

Informal description

For any two generalized Heyting algebras $\alpha$ and $\beta$, the product $\alpha \times \beta$ is also a generalized Heyting algebra, with the Heyting implication and order structure defined componentwise.

Pi.instGeneralizedHeytingAlgebra instance

{α : ι → Type*} [∀ i, GeneralizedHeytingAlgebra (α i)] : GeneralizedHeytingAlgebra (∀ i, α i)

Full source

instance Pi.instGeneralizedHeytingAlgebra {α : ι → Type*} [∀ i, GeneralizedHeytingAlgebra (α i)] :
    GeneralizedHeytingAlgebra (∀ i, α i) where
  le_himp_iff i := by simp [le_def]

Pointwise Generalized Heyting Algebra Structure on Product Types

Informal description

For any family of types $(\alpha_i)_{i \in \iota}$ where each $\alpha_i$ is a generalized Heyting algebra, the product type $\forall i, \alpha_i$ is also a generalized Heyting algebra with the Heyting implication defined pointwise.

sdiff_le_iff theorem

: a \ b ≤ c ↔ a ≤ b ⊔ c

Full source

@[simp]
theorem sdiff_le_iff : a \ ba \ b ≤ c ↔ a ≤ b ⊔ c :=
  GeneralizedCoheytingAlgebra.sdiff_le_iff _ _ _

Characterization of Difference in Co-Heyting Algebras: $a \setminus b \leq c \leftrightarrow a \leq b \sqcup c$

Informal description

In a generalized co-Heyting algebra, for any elements $a, b, c$, the inequality $a \setminus b \leq c$ holds if and only if $a \leq b \sqcup c$.

sdiff_le_iff' theorem

: a \ b ≤ c ↔ a ≤ c ⊔ b

Full source

theorem sdiff_le_iff' : a \ ba \ b ≤ c ↔ a ≤ c ⊔ b := by rw [sdiff_le_iff, sup_comm]

Alternative Characterization of Difference in Co-Heyting Algebras: $a \setminus b \leq c \leftrightarrow a \leq c \sqcup b$

Informal description

In a generalized co-Heyting algebra, for any elements $a, b, c$, the inequality $a \setminus b \leq c$ holds if and only if $a \leq c \sqcup b$.

sdiff_le_comm theorem

: a \ b ≤ c ↔ a \ c ≤ b

Full source

theorem sdiff_le_comm : a \ ba \ b ≤ c ↔ a \ c ≤ b := by rw [sdiff_le_iff, sdiff_le_iff']

Commutativity of Difference in Co-Heyting Algebras: $a \setminus b \leq c \leftrightarrow a \setminus c \leq b$

Informal description

In a generalized co-Heyting algebra, for any elements $a$, $b$, and $c$, the inequality $a \setminus b \leq c$ holds if and only if $a \setminus c \leq b$.

sdiff_le theorem

: a \ b ≤ a

Full source

theorem sdiff_le : a \ b ≤ a :=
  sdiff_le_iff.2 le_sup_right

Difference is Less Than Original in Co-Heyting Algebras

Informal description

In a generalized co-Heyting algebra, for any elements $a$ and $b$, the difference $a \setminus b$ is less than or equal to $a$, i.e., $a \setminus b \leq a$.

Disjoint.disjoint_sdiff_left theorem

(h : Disjoint a b) : Disjoint (a \ c) b

Full source

theorem Disjoint.disjoint_sdiff_left (h : Disjoint a b) : Disjoint (a \ c) b :=
  h.mono_left sdiff_le

Disjointness Preservation Under Left Difference in Co-Heyting Algebras

Informal description

For any elements $a$, $b$, and $c$ in a generalized co-Heyting algebra, if $a$ and $b$ are disjoint (i.e., $a \sqcap b = \bot$), then the difference $a \setminus c$ and $b$ are also disjoint, i.e., $(a \setminus c) \sqcap b = \bot$.

Disjoint.disjoint_sdiff_right theorem

(h : Disjoint a b) : Disjoint a (b \ c)

Full source

theorem Disjoint.disjoint_sdiff_right (h : Disjoint a b) : Disjoint a (b \ c) :=
  h.mono_right sdiff_le

Disjointness Preservation Under Right Difference in Co-Heyting Algebras

Informal description

In a generalized co-Heyting algebra, if two elements $a$ and $b$ are disjoint (i.e., $a \sqcap b = \bot$), then $a$ is also disjoint with the difference $b \setminus c$ for any element $c$.

sdiff_le_iff_left theorem

: a \ b ≤ b ↔ a ≤ b

Full source

theorem sdiff_le_iff_left : a \ ba \ b ≤ b ↔ a ≤ b := by rw [sdiff_le_iff, sup_idem]

Characterization of Difference Inequality: $a \setminus b \leq b \leftrightarrow a \leq b$

Informal description

In a generalized co-Heyting algebra, for any elements $a$ and $b$, the inequality $a \setminus b \leq b$ holds if and only if $a \leq b$.

sdiff_self theorem

: a \ a = ⊥

Full source

@[simp]
theorem sdiff_self : a \ a = ⊥ :=
  le_bot_iff.1 <| sdiff_le_iff.2 le_sup_left

Self-Difference Equals Bottom: $a \setminus a = \bot$

Informal description

For any element $a$ in a generalized co-Heyting algebra, the difference $a \setminus a$ equals the bottom element $\bot$.

le_sup_sdiff theorem

: a ≤ b ⊔ a \ b

Full source

theorem le_sup_sdiff : a ≤ b ⊔ a \ b :=
  sdiff_le_iff.1 le_rfl

Join-Difference Inequality in Co-Heyting Algebras: $a \leq b \sqcup (a \setminus b)$

Informal description

In a generalized co-Heyting algebra, for any elements $a$ and $b$, the inequality $a \leq b \sqcup (a \setminus b)$ holds.

le_sdiff_sup theorem

: a ≤ a \ b ⊔ b

Full source

theorem le_sdiff_sup : a ≤ a \ ba \ b ⊔ b := by rw [sup_comm, ← sdiff_le_iff]

Inequality Relating Difference and Join in Co-Heyting Algebras: $a \leq a \setminus b \sqcup b$

Informal description

In a generalized co-Heyting algebra, for any elements $a$ and $b$, the inequality $a \leq a \setminus b \sqcup b$ holds.

sup_sdiff_left theorem

: a ⊔ a \ b = a

Full source

theorem sup_sdiff_left : a ⊔ a \ b = a :=
  sup_of_le_left sdiff_le

Join-Difference Identity in Co-Heyting Algebras: $a \sqcup (a \setminus b) = a$

Informal description

In a generalized co-Heyting algebra, for any elements $a$ and $b$, the join of $a$ and the difference $a \setminus b$ equals $a$, i.e., $a \sqcup (a \setminus b) = a$.

sup_sdiff_right theorem

: a \ b ⊔ a = a

Full source

theorem sup_sdiff_right : a \ ba \ b ⊔ a = a :=
  sup_of_le_right sdiff_le

Join with Difference Preserves Original Element in Co-Heyting Algebras

Informal description

In a generalized co-Heyting algebra, for any elements $a$ and $b$, the join of the difference $a \setminus b$ and $a$ equals $a$, i.e., $(a \setminus b) \sqcup a = a$.

inf_sdiff_left theorem

: a \ b ⊓ a = a \ b

Full source

theorem inf_sdiff_left : a \ ba \ b ⊓ a = a \ b :=
  inf_of_le_left sdiff_le

Meet with Original Preserves Difference in Co-Heyting Algebras

Informal description

In a generalized co-Heyting algebra, for any elements $a$ and $b$, the meet of $a \setminus b$ and $a$ equals $a \setminus b$, i.e., $(a \setminus b) \sqcap a = a \setminus b$.

inf_sdiff_right theorem

: a ⊓ a \ b = a \ b

Full source

theorem inf_sdiff_right : a ⊓ a \ b = a \ b :=
  inf_of_le_right sdiff_le

Meet with Difference Equals Difference in Co-Heyting Algebras

Informal description

In a generalized co-Heyting algebra, for any elements $a$ and $b$, the meet of $a$ and the difference $a \setminus b$ equals the difference itself, i.e., $a \sqcap (a \setminus b) = a \setminus b$.

sup_sdiff_self theorem

(a b : α) : a ⊔ b \ a = a ⊔ b

Full source

@[simp]
theorem sup_sdiff_self (a b : α) : a ⊔ b \ a = a ⊔ b :=
  le_antisymm (sup_le_sup_left sdiff_le _) (sup_le le_sup_left le_sup_sdiff)

Join-Difference Identity in Co-Heyting Algebras: $a \sqcup (b \setminus a) = a \sqcup b$

Informal description

In a generalized co-Heyting algebra, for any elements $a$ and $b$, the join of $a$ and the difference $b \setminus a$ equals the join of $a$ and $b$, i.e., $a \sqcup (b \setminus a) = a \sqcup b$.

sdiff_sup_self theorem

(a b : α) : b \ a ⊔ a = b ⊔ a

Full source

@[simp]
theorem sdiff_sup_self (a b : α) : b \ ab \ a ⊔ a = b ⊔ a := by rw [sup_comm, sup_sdiff_self, sup_comm]

Difference-Join Identity in Co-Heyting Algebras: $(b \setminus a) \sqcup a = b \sqcup a$

Informal description

In a generalized co-Heyting algebra, for any elements $a$ and $b$, the join of the difference $b \setminus a$ and $a$ equals the join of $b$ and $a$, i.e., $(b \setminus a) \sqcup a = b \sqcup a$.

sup_sdiff_eq_sup theorem

(h : c ≤ a) : a ⊔ b \ c = a ⊔ b

Full source

theorem sup_sdiff_eq_sup (h : c ≤ a) : a ⊔ b \ c = a ⊔ b :=
  sup_congr_left (sdiff_le.trans le_sup_right) <| le_sup_sdiff.trans <| sup_le_sup_right h _

Join-Difference Equality under Lower Bound Condition: $a \sqcup (b \setminus c) = a \sqcup b$ when $c \leq a$

Informal description

In a generalized co-Heyting algebra, for any elements $a$, $b$, and $c$ such that $c \leq a$, the equality $a \sqcup (b \setminus c) = a \sqcup b$ holds.

sup_sdiff_cancel' theorem

(hab : a ≤ b) (hbc : b ≤ c) : b ⊔ c \ a = c

Full source

theorem sup_sdiff_cancel' (hab : a ≤ b) (hbc : b ≤ c) : b ⊔ c \ a = c := by
  rw [sup_sdiff_eq_sup hab, sup_of_le_right hbc]

Join-Difference Cancellation under Chain Condition: $b \sqcup (c \setminus a) = c$ when $a \leq b \leq c$

Informal description

In a generalized co-Heyting algebra, for any elements $a$, $b$, and $c$ such that $a \leq b \leq c$, the equality $b \sqcup (c \setminus a) = c$ holds.

sup_sdiff_cancel_right theorem

(h : a ≤ b) : a ⊔ b \ a = b

Full source

theorem sup_sdiff_cancel_right (h : a ≤ b) : a ⊔ b \ a = b :=
  sup_sdiff_cancel' le_rfl h

Right cancellation law for join and difference: $a \sqcup (b \setminus a) = b$ when $a \leq b$

Informal description

In a generalized co-Heyting algebra, for any elements $a$ and $b$ such that $a \leq b$, the equality $a \sqcup (b \setminus a) = b$ holds.

sdiff_sup_cancel theorem

(h : b ≤ a) : a \ b ⊔ b = a

Full source

theorem sdiff_sup_cancel (h : b ≤ a) : a \ ba \ b ⊔ b = a := by rw [sup_comm, sup_sdiff_cancel_right h]

Difference-Join Cancellation: $(a \setminus b) \sqcup b = a$ when $b \leq a$

Informal description

In a generalized co-Heyting algebra, for any elements $a$ and $b$ such that $b \leq a$, the equality $(a \setminus b) \sqcup b = a$ holds.

sup_le_of_le_sdiff_left theorem

(h : b ≤ c \ a) (hac : a ≤ c) : a ⊔ b ≤ c

Full source

theorem sup_le_of_le_sdiff_left (h : b ≤ c \ a) (hac : a ≤ c) : a ⊔ b ≤ c :=
  sup_le hac <| h.trans sdiff_le

Supremum Bound via Difference Inequality

Informal description

In a generalized co-Heyting algebra, for any elements $a, b, c$, if $b \leq c \setminus a$ and $a \leq c$, then $a \sqcup b \leq c$.

sup_le_of_le_sdiff_right theorem

(h : a ≤ c \ b) (hbc : b ≤ c) : a ⊔ b ≤ c

Full source

theorem sup_le_of_le_sdiff_right (h : a ≤ c \ b) (hbc : b ≤ c) : a ⊔ b ≤ c :=
  sup_le (h.trans sdiff_le) hbc

Supremum bound via right difference condition

Informal description

In a generalized co-Heyting algebra, for any elements $a, b, c$, if $a \leq c \setminus b$ and $b \leq c$, then $a \sqcup b \leq c$.

sdiff_eq_bot_iff theorem

: a \ b = ⊥ ↔ a ≤ b

Full source

@[simp]
theorem sdiff_eq_bot_iff : a \ ba \ b = ⊥ ↔ a ≤ b := by rw [← le_bot_iff, sdiff_le_iff, sup_bot_eq]

Characterization of Difference Equals Bottom: $a \setminus b = \bot \leftrightarrow a \leq b$

Informal description

In a generalized co-Heyting algebra, for any elements $a$ and $b$, the difference $a \setminus b$ equals the bottom element $\bot$ if and only if $a$ is less than or equal to $b$.

sdiff_bot theorem

: a \ ⊥ = a

Full source

@[simp]
theorem sdiff_bot : a \ ⊥ = a :=
  eq_of_forall_ge_iff fun b => by rw [sdiff_le_iff, bot_sup_eq]

Difference with Bottom Element: $a \setminus \bot = a$

Informal description

In a generalized co-Heyting algebra, for any element $a$, the difference $a \setminus \bot$ equals $a$, i.e., $a \setminus \bot = a$.

bot_sdiff theorem

: ⊥ \ a = ⊥

Full source

@[simp]
theorem bot_sdiff : ⊥⊥ \ a = ⊥ :=
  sdiff_eq_bot_iff.2 bot_le

Bottom Difference Identity: $\bot \setminus a = \bot$

Informal description

In a generalized co-Heyting algebra, the difference between the bottom element $\bot$ and any element $a$ is equal to $\bot$, i.e., $\bot \setminus a = \bot$.

sdiff_sdiff_sdiff_le_sdiff theorem

: (a \ b) \ (a \ c) ≤ c \ b

Full source

theorem sdiff_sdiff_sdiff_le_sdiff : (a \ b) \ (a \ c) ≤ c \ b := by
  rw [sdiff_le_iff, sdiff_le_iff, sup_left_comm, sup_sdiff_self, sup_left_comm, sdiff_sup_self,
    sup_left_comm]
  exact le_sup_left

Difference Inequality in Co-Heyting Algebras: $(a \setminus b) \setminus (a \setminus c) \leq c \setminus b$

Informal description

In a generalized co-Heyting algebra, for any elements $a, b, c$, the following inequality holds: $$(a \setminus b) \setminus (a \setminus c) \leq c \setminus b.$$

le_sup_sdiff_sup_sdiff theorem

: a ≤ b ⊔ (a \ c ⊔ c \ b)

Full source

@[simp]
theorem le_sup_sdiff_sup_sdiff : a ≤ b ⊔ (a \ c ⊔ c \ b) := by
  simpa using @sdiff_sdiff_sdiff_le_sdiff

Inequality Relating Union and Difference in Co-Heyting Algebras: $a \leq b \sqcup (a \setminus c \sqcup c \setminus b)$

Informal description

In a generalized co-Heyting algebra, for any elements $a, b, c$, the following inequality holds: $$a \leq b \sqcup (a \setminus c \sqcup c \setminus b).$$

sdiff_sdiff theorem

(a b c : α) : (a \ b) \ c = a \ (b ⊔ c)

Full source

theorem sdiff_sdiff (a b c : α) : (a \ b) \ c = a \ (b ⊔ c) :=
  eq_of_forall_ge_iff fun d => by simp_rw [sdiff_le_iff, sup_assoc]

Double Difference Equals Difference of Union in Co-Heyting Algebra

Informal description

In a generalized co-Heyting algebra $\alpha$, for any elements $a, b, c \in \alpha$, the double difference operation satisfies $(a \setminus b) \setminus c = a \setminus (b \sqcup c)$.

sdiff_sdiff_left theorem

: (a \ b) \ c = a \ (b ⊔ c)

Full source

theorem sdiff_sdiff_left : (a \ b) \ c = a \ (b ⊔ c) :=
  sdiff_sdiff _ _ _

Double Difference Equals Difference of Union in Co-Heyting Algebra

Informal description

In a generalized co-Heyting algebra $\alpha$, for any elements $a, b, c \in \alpha$, the double difference operation satisfies $(a \setminus b) \setminus c = a \setminus (b \sqcup c)$.

sdiff_right_comm theorem

(a b c : α) : (a \ b) \ c = (a \ c) \ b

Full source

theorem sdiff_right_comm (a b c : α) : (a \ b) \ c = (a \ c) \ b := by
  simp_rw [sdiff_sdiff, sup_comm]

Right Commutativity of Difference Operation in Co-Heyting Algebra

Informal description

In a generalized co-Heyting algebra $\alpha$, for any elements $a, b, c \in \alpha$, the difference operation satisfies $(a \setminus b) \setminus c = (a \setminus c) \setminus b$.

sdiff_sdiff_comm theorem

: (a \ b) \ c = (a \ c) \ b

Full source

theorem sdiff_sdiff_comm : (a \ b) \ c = (a \ c) \ b :=
  sdiff_right_comm _ _ _

Commutativity of Double Difference in Co-Heyting Algebra

Informal description

In a generalized co-Heyting algebra $\alpha$, for any elements $a, b, c \in \alpha$, the double difference operation satisfies $(a \setminus b) \setminus c = (a \setminus c) \setminus b$.

sdiff_idem theorem

: (a \ b) \ b = a \ b

Full source

@[simp]
theorem sdiff_idem : (a \ b) \ b = a \ b := by rw [sdiff_sdiff_left, sup_idem]

Idempotence of Double Difference in Co-Heyting Algebra

Informal description

In a generalized co-Heyting algebra $\alpha$, for any elements $a, b \in \alpha$, the double difference operation satisfies $(a \setminus b) \setminus b = a \setminus b$.

sdiff_sdiff_self theorem

: (a \ b) \ a = ⊥

Full source

@[simp]
theorem sdiff_sdiff_self : (a \ b) \ a = ⊥ := by rw [sdiff_sdiff_comm, sdiff_self, bot_sdiff]

Double Difference Identity: $(a \setminus b) \setminus a = \bot$

Informal description

In a generalized co-Heyting algebra, for any elements $a$ and $b$, the double difference operation satisfies $(a \setminus b) \setminus a = \bot$.

sup_sdiff_distrib theorem

(a b c : α) : (a ⊔ b) \ c = a \ c ⊔ b \ c

Full source

theorem sup_sdiff_distrib (a b c : α) : (a ⊔ b) \ c = a \ ca \ c ⊔ b \ c :=
  eq_of_forall_ge_iff fun d => by simp_rw [sdiff_le_iff, sup_le_iff, sdiff_le_iff]

Distributivity of difference over join in co-Heyting algebras

Informal description

In a generalized co-Heyting algebra $\alpha$, for any elements $a, b, c \in \alpha$, the difference operation distributes over the join operation as follows: $$(a \sqcup b) \setminus c = (a \setminus c) \sqcup (b \setminus c).$$

sdiff_inf_distrib theorem

(a b c : α) : a \ (b ⊓ c) = a \ b ⊔ a \ c

Full source

theorem sdiff_inf_distrib (a b c : α) : a \ (b ⊓ c) = a \ ba \ b ⊔ a \ c :=
  eq_of_forall_ge_iff fun d => by
    rw [sup_le_iff, sdiff_le_comm, le_inf_iff]
    simp_rw [sdiff_le_comm]

Distributivity of difference over meet in co-Heyting algebras: $a \setminus (b \sqcap c) = (a \setminus b) \sqcup (a \setminus c)$

Informal description

In a generalized co-Heyting algebra $\alpha$, for any elements $a, b, c \in \alpha$, the difference operation distributes over the meet operation as follows: $$a \setminus (b \sqcap c) = (a \setminus b) \sqcup (a \setminus c).$$

sup_sdiff theorem

: (a ⊔ b) \ c = a \ c ⊔ b \ c

Full source

theorem sup_sdiff : (a ⊔ b) \ c = a \ ca \ c ⊔ b \ c :=
  sup_sdiff_distrib _ _ _

Distributivity of difference over join in co-Heyting algebras

Informal description

In a generalized co-Heyting algebra, for any elements $a, b, c$, the difference operation distributes over the join operation as: $$(a \sqcup b) \setminus c = (a \setminus c) \sqcup (b \setminus c).$$

sup_sdiff_right_self theorem

: (a ⊔ b) \ b = a \ b

Full source

@[simp]
theorem sup_sdiff_right_self : (a ⊔ b) \ b = a \ b := by rw [sup_sdiff, sdiff_self, sup_bot_eq]

Right Self-Difference Identity in Co-Heyting Algebras: $(a \sqcup b) \setminus b = a \setminus b$

Informal description

In a generalized co-Heyting algebra, for any elements $a$ and $b$, the difference of their join with $b$ equals the difference of $a$ with $b$, i.e., $(a \sqcup b) \setminus b = a \setminus b$.

sup_sdiff_left_self theorem

: (a ⊔ b) \ a = b \ a

Full source

@[simp]
theorem sup_sdiff_left_self : (a ⊔ b) \ a = b \ a := by rw [sup_comm, sup_sdiff_right_self]

Left Self-Difference Identity in Co-Heyting Algebras: $(a \sqcup b) \setminus a = b \setminus a$

Informal description

In a generalized co-Heyting algebra, for any elements $a$ and $b$, the difference of their join with $a$ equals the difference of $b$ with $a$, i.e., $(a \sqcup b) \setminus a = b \setminus a$.

sdiff_le_sdiff_right theorem

(h : a ≤ b) : a \ c ≤ b \ c

Full source

@[gcongr]
theorem sdiff_le_sdiff_right (h : a ≤ b) : a \ c ≤ b \ c :=
  sdiff_le_iff.2 <| h.trans <| le_sup_sdiff

Monotonicity of Difference in Co-Heyting Algebras: $a \leq b \Rightarrow a \setminus c \leq b \setminus c$

Informal description

In a generalized co-Heyting algebra, if $a \leq b$, then $a \setminus c \leq b \setminus c$ for any element $c$.

sdiff_le_sdiff_left theorem

(h : a ≤ b) : c \ b ≤ c \ a

Full source

@[gcongr]
theorem sdiff_le_sdiff_left (h : a ≤ b) : c \ b ≤ c \ a :=
  sdiff_le_iff.2 <| le_sup_sdiff.trans <| sup_le_sup_right h _

Monotonicity of Difference with Respect to Right Argument: $a \leq b \implies c \setminus b \leq c \setminus a$

Informal description

In a generalized co-Heyting algebra, if $a \leq b$, then for any element $c$, the difference $c \setminus b$ is less than or equal to $c \setminus a$.

sdiff_le_sdiff theorem

(hab : a ≤ b) (hcd : c ≤ d) : a \ d ≤ b \ c

Full source

@[gcongr]
theorem sdiff_le_sdiff (hab : a ≤ b) (hcd : c ≤ d) : a \ d ≤ b \ c :=
  (sdiff_le_sdiff_right hab).trans <| sdiff_le_sdiff_left hcd

Monotonicity of Difference in Co-Heyting Algebras: $a \leq b \land c \leq d \Rightarrow a \setminus d \leq b \setminus c$

Informal description

In a generalized co-Heyting algebra, for any elements $a, b, c, d$ such that $a \leq b$ and $c \leq d$, the difference $a \setminus d$ is less than or equal to $b \setminus c$.

sdiff_inf theorem

: a \ (b ⊓ c) = a \ b ⊔ a \ c

Full source

theorem sdiff_inf : a \ (b ⊓ c) = a \ ba \ b ⊔ a \ c :=
  sdiff_inf_distrib _ _ _

Distributivity of difference over meet: $a \setminus (b \sqcap c) = (a \setminus b) \sqcup (a \setminus c)$

Informal description

In a generalized co-Heyting algebra, for any elements $a, b, c$, the difference operation distributes over the meet operation as: $$a \setminus (b \sqcap c) = (a \setminus b) \sqcup (a \setminus c).$$

sdiff_inf_self_left theorem

(a b : α) : a \ (a ⊓ b) = a \ b

Full source

@[simp]
theorem sdiff_inf_self_left (a b : α) : a \ (a ⊓ b) = a \ b := by
  rw [sdiff_inf, sdiff_self, bot_sup_eq]

Difference of Element and Its Meet with Another Equals Their Difference: $a \setminus (a \sqcap b) = a \setminus b$

Informal description

In a generalized co-Heyting algebra, for any elements $a$ and $b$, the difference of $a$ and the meet of $a$ and $b$ equals the difference of $a$ and $b$, i.e., $$ a \setminus (a \sqcap b) = a \setminus b. $$

sdiff_inf_self_right theorem

(a b : α) : b \ (a ⊓ b) = b \ a

Full source

@[simp]
theorem sdiff_inf_self_right (a b : α) : b \ (a ⊓ b) = b \ a := by
  rw [sdiff_inf, sdiff_self, sup_bot_eq]

Right Self-Difference of Meet Equals Difference: $b \setminus (a \sqcap b) = b \setminus a$

Informal description

In a generalized co-Heyting algebra, for any elements $a$ and $b$, the difference of $b$ and the meet of $a$ and $b$ equals the difference of $b$ and $a$, i.e., $$ b \setminus (a \sqcap b) = b \setminus a. $$

Disjoint.sdiff_eq_left theorem

(h : Disjoint a b) : a \ b = a

Full source

theorem Disjoint.sdiff_eq_left (h : Disjoint a b) : a \ b = a := by
  conv_rhs => rw [← @sdiff_bot _ _ a]
  rw [← h.eq_bot, sdiff_inf_self_left]

Difference of Disjoint Elements: $a \setminus b = a$ when $a$ and $b$ are disjoint

Informal description

For any two elements $a$ and $b$ in a generalized co-Heyting algebra, if $a$ and $b$ are disjoint (i.e., $a \sqcap b = \bot$), then the difference $a \setminus b$ equals $a$.

Disjoint.sdiff_eq_right theorem

(h : Disjoint a b) : b \ a = b

Full source

theorem Disjoint.sdiff_eq_right (h : Disjoint a b) : b \ a = b :=
  h.symm.sdiff_eq_left

Difference of Disjoint Elements: $b \setminus a = b$ when $a$ and $b$ are disjoint

Informal description

For any two elements $a$ and $b$ in a generalized co-Heyting algebra, if $a$ and $b$ are disjoint (i.e., $a \sqcap b = \bot$), then the difference $b \setminus a$ equals $b$.

Disjoint.sup_sdiff_cancel_left theorem

(h : Disjoint a b) : (a ⊔ b) \ a = b

Full source

theorem Disjoint.sup_sdiff_cancel_left (h : Disjoint a b) : (a ⊔ b) \ a = b := by
  rw [sup_sdiff, sdiff_self, bot_sup_eq, h.sdiff_eq_right]

Left Cancellation of Join with Difference for Disjoint Elements: $(a \sqcup b) \setminus a = b$ when $a \sqcap b = \bot$

Informal description

For any two elements $a$ and $b$ in a generalized co-Heyting algebra, if $a$ and $b$ are disjoint (i.e., $a \sqcap b = \bot$), then the difference of their join and $a$ equals $b$, i.e., $(a \sqcup b) \setminus a = b$.

Disjoint.sup_sdiff_cancel_right theorem

(h : Disjoint a b) : (a ⊔ b) \ b = a

Full source

theorem Disjoint.sup_sdiff_cancel_right (h : Disjoint a b) : (a ⊔ b) \ b = a := by
  rw [sup_sdiff, sdiff_self, sup_bot_eq, h.sdiff_eq_left]

Right Cancellation of Join with Difference for Disjoint Elements: $(a \sqcup b) \setminus b = a$ when $a \sqcap b = \bot$

Informal description

In a generalized co-Heyting algebra, if two elements $a$ and $b$ are disjoint (i.e., $a \sqcap b = \bot$), then the difference of their join and $b$ equals $a$, i.e., $(a \sqcup b) \setminus b = a$.

Disjoint.le_sdiff_of_le_left theorem

(hac : Disjoint a c) (hab : a ≤ b) : a ≤ b \ c

Full source

/-- See `le_sdiff` for a stronger version in generalised Boolean algebras. -/
theorem Disjoint.le_sdiff_of_le_left (hac : Disjoint a c) (hab : a ≤ b) : a ≤ b \ c :=
  hac.sdiff_eq_left.ge.trans <| sdiff_le_sdiff_right hab

Disjointness and Order Imply Difference Inequality in Co-Heyting Algebras

Informal description

Let $\alpha$ be a generalized co-Heyting algebra. For any elements $a, b, c \in \alpha$, if $a$ and $c$ are disjoint (i.e., $a \sqcap c = \bot$) and $a \leq b$, then $a \leq b \setminus c$.

sdiff_sdiff_le theorem

: a \ (a \ b) ≤ b

Full source

theorem sdiff_sdiff_le : a \ (a \ b) ≤ b :=
  sdiff_le_iff.2 le_sdiff_sup

Double Difference Inequality in Co-Heyting Algebras: $a \setminus (a \setminus b) \leq b$

Informal description

In a generalized co-Heyting algebra, for any elements $a$ and $b$, the double difference $a \setminus (a \setminus b)$ is less than or equal to $b$.

sdiff_eq_sdiff_iff theorem

: a \ b = b \ a ↔ a = b

Full source

@[simp] lemma sdiff_eq_sdiff_iff : a \ ba \ b = b \ a ↔ a = b := by simp [le_antisymm_iff]

Equality of Differences is Equivalent to Element Equality in Co-Heyting Algebras

Informal description

For any elements $a$ and $b$ in a generalized co-Heyting algebra, the difference operations are equal ($a \setminus b = b \setminus a$) if and only if $a = b$.

sdiff_ne_sdiff_iff theorem

: a \ b ≠ b \ a ↔ a ≠ b

Full source

lemma sdiff_ne_sdiff_iff : a \ ba \ b ≠ b \ aa \ b ≠ b \ a ↔ a ≠ b := sdiff_eq_sdiff_iff.not

Inequality of Differences is Equivalent to Element Inequality in Co-Heyting Algebras

Informal description

For any elements $a$ and $b$ in a generalized co-Heyting algebra, the difference operations are unequal ($a \setminus b \neq b \setminus a$) if and only if $a \neq b$.

sdiff_triangle theorem

(a b c : α) : a \ c ≤ a \ b ⊔ b \ c

Full source

theorem sdiff_triangle (a b c : α) : a \ c ≤ a \ ba \ b ⊔ b \ c := by
  rw [sdiff_le_iff, sup_left_comm, ← sdiff_le_iff]
  exact sdiff_sdiff_le.trans le_sup_sdiff

Triangle Inequality for Differences in Co-Heyting Algebras: $a \setminus c \leq (a \setminus b) \sqcup (b \setminus c)$

Informal description

For any elements $a$, $b$, and $c$ in a generalized co-Heyting algebra, the difference $a \setminus c$ is less than or equal to the join of the differences $a \setminus b$ and $b \setminus c$, i.e., $$ a \setminus c \leq (a \setminus b) \sqcup (b \setminus c). $$

sdiff_sup_sdiff_cancel theorem

(hba : b ≤ a) (hcb : c ≤ b) : a \ b ⊔ b \ c = a \ c

Full source

theorem sdiff_sup_sdiff_cancel (hba : b ≤ a) (hcb : c ≤ b) : a \ ba \ b ⊔ b \ c = a \ c :=
  (sdiff_triangle _ _ _).antisymm' <| sup_le (sdiff_le_sdiff_left hcb) (sdiff_le_sdiff_right hba)

Cancellation Law for Differences in Co-Heyting Algebras: $(a \setminus b) \sqcup (b \setminus c) = a \setminus c$ under $b \leq a$ and $c \leq b$

Informal description

In a generalized co-Heyting algebra, if $b \leq a$ and $c \leq b$, then $(a \setminus b) \sqcup (b \setminus c) = a \setminus c$.

sdiff_sup_sdiff_cancel' theorem

(hinf : a ⊓ c ≤ b) (hsup : b ≤ a ⊔ c) : a \ b ⊔ b \ c = a \ c

Full source

/-- a version of `sdiff_sup_sdiff_cancel` with more general hypotheses. -/
theorem sdiff_sup_sdiff_cancel' (hinf : a ⊓ c ≤ b) (hsup : b ≤ a ⊔ c) :
    a \ ba \ b ⊔ b \ c = a \ c := by
  refine (sdiff_triangle ..).antisymm' <| sup_le ?_ <| by simpa [sup_comm]
  rw [← sdiff_inf_self_left (b := c)]
  exact sdiff_le_sdiff_left hinf

Generalized Difference Cancellation: $(a \setminus b) \sqcup (b \setminus c) = a \setminus c$ under $a \sqcap c \leq b \leq a \sqcup c$

Informal description

In a generalized co-Heyting algebra, for any elements $a$, $b$, and $c$ such that $a \sqcap c \leq b$ and $b \leq a \sqcup c$, it holds that $(a \setminus b) \sqcup (b \setminus c) = a \setminus c$.

sdiff_le_sdiff_of_sup_le_sup_left theorem

(h : c ⊔ a ≤ c ⊔ b) : a \ c ≤ b \ c

Full source

theorem sdiff_le_sdiff_of_sup_le_sup_left (h : c ⊔ a ≤ c ⊔ b) : a \ c ≤ b \ c := by
  rw [← sup_sdiff_left_self, ← @sup_sdiff_left_self _ _ _ b]
  exact sdiff_le_sdiff_right h

Left Join Order Preserves Difference: $c \sqcup a \leq c \sqcup b \Rightarrow a \setminus c \leq b \setminus c$

Informal description

In a generalized co-Heyting algebra, if $c \sqcup a \leq c \sqcup b$ for elements $a, b, c$, then the difference $a \setminus c$ is less than or equal to $b \setminus c$.

sdiff_le_sdiff_of_sup_le_sup_right theorem

(h : a ⊔ c ≤ b ⊔ c) : a \ c ≤ b \ c

Full source

theorem sdiff_le_sdiff_of_sup_le_sup_right (h : a ⊔ c ≤ b ⊔ c) : a \ c ≤ b \ c := by
  rw [← sup_sdiff_right_self, ← @sup_sdiff_right_self _ _ b]
  exact sdiff_le_sdiff_right h

Right Join Order Preserves Difference: $a \sqcup c \leq b \sqcup c \Rightarrow a \setminus c \leq b \setminus c$

Informal description

In a generalized co-Heyting algebra, if $a \sqcup c \leq b \sqcup c$ for elements $a, b, c$, then the difference $a \setminus c$ is less than or equal to $b \setminus c$.

inf_sdiff_sup_left theorem

: a \ c ⊓ (a ⊔ b) = a \ c

Full source

@[simp]
theorem inf_sdiff_sup_left : a \ ca \ c ⊓ (a ⊔ b) = a \ c :=
  inf_of_le_left <| sdiff_le.trans le_sup_left

Difference-Meet-Join Identity in Co-Heyting Algebras

Informal description

In a generalized co-Heyting algebra, for any elements $a$, $b$, and $c$, the meet of the difference $a \setminus c$ and the join $a \sqcup b$ equals $a \setminus c$, i.e., $(a \setminus c) \sqcap (a \sqcup b) = a \setminus c$.

inf_sdiff_sup_right theorem

: a \ c ⊓ (b ⊔ a) = a \ c

Full source

@[simp]
theorem inf_sdiff_sup_right : a \ ca \ c ⊓ (b ⊔ a) = a \ c :=
  inf_of_le_left <| sdiff_le.trans le_sup_right

Difference-Meet-Join Identity in Co-Heyting Algebras

Informal description

In a generalized co-Heyting algebra, for any elements $a$, $b$, and $c$, the meet of the difference $a \setminus c$ and the join $b \sqcup a$ equals $a \setminus c$, i.e., $(a \setminus c) \sqcap (b \sqcup a) = a \setminus c$.

gc_sdiff_sup theorem

: GaloisConnection (· \ a) (a ⊔ ·)

Full source

theorem gc_sdiff_sup : GaloisConnection (· \ a) (a ⊔ ·) :=
  fun _ _ ↦ sdiff_le_iff

Galois Connection Between Difference and Join in Co-Heyting Algebras

Informal description

In a generalized co-Heyting algebra, for any element $a$, the pair of operations $(· \setminus a, a \sqcup ·)$ forms a Galois connection. That is, for any elements $b$ and $c$, we have $b \setminus a \leq c$ if and only if $b \leq a \sqcup c$.

GeneralizedCoheytingAlgebra.toDistribLattice instance

: DistribLattice α

Full source

instance (priority := 100) GeneralizedCoheytingAlgebra.toDistribLattice : DistribLattice α :=
  { ‹GeneralizedCoheytingAlgebra α› with
    le_sup_inf :=
      fun a b c => by simp_rw [← sdiff_le_iff, le_inf_iff, sdiff_le_iff, ← le_inf_iff]; rfl }

Generalized Co-Heyting Algebras are Distributive Lattices

Informal description

Every generalized co-Heyting algebra is a distributive lattice.

OrderDual.instGeneralizedHeytingAlgebra instance

: GeneralizedHeytingAlgebra αᵒᵈ

Full source

instance OrderDual.instGeneralizedHeytingAlgebra : GeneralizedHeytingAlgebra αᵒᵈ where
  himp := fun a b => toDual (ofDualofDual b \ ofDual a)
  le_himp_iff := fun a b c => by rw [inf_comm]; exact sdiff_le_iff

Order Dual of a Generalized Heyting Algebra is a Generalized Heyting Algebra

Informal description

For any generalized Heyting algebra $\alpha$, the order dual $\alpha^{\text{op}}$ is also a generalized Heyting algebra. This means that if $\alpha$ is a lattice with a top element $\top$ and a Heyting implication operation $\Rightarrow$ satisfying $a \sqcap b \leq c \leftrightarrow a \leq (b \Rightarrow c)$, then the same structure holds in the opposite order on $\alpha^{\text{op}}$.

Prod.instGeneralizedCoheytingAlgebra instance

[GeneralizedCoheytingAlgebra β] : GeneralizedCoheytingAlgebra (α × β)

Full source

instance Prod.instGeneralizedCoheytingAlgebra [GeneralizedCoheytingAlgebra β] :
    GeneralizedCoheytingAlgebra (α × β) where
  sdiff_le_iff _ _ _ := and_congr sdiff_le_iff sdiff_le_iff

Generalized Co-Heyting Algebra Structure on Product Types

Informal description

For any generalized co-Heyting algebras $\alpha$ and $\beta$, the product type $\alpha \times \beta$ is also a generalized co-Heyting algebra, where the lattice operations, bottom element, and difference operation are defined componentwise.

Pi.instGeneralizedCoheytingAlgebra instance

{α : ι → Type*} [∀ i, GeneralizedCoheytingAlgebra (α i)] : GeneralizedCoheytingAlgebra (∀ i, α i)

Full source

instance Pi.instGeneralizedCoheytingAlgebra {α : ι → Type*}
    [∀ i, GeneralizedCoheytingAlgebra (α i)] : GeneralizedCoheytingAlgebra (∀ i, α i) where
  sdiff_le_iff i := by simp [le_def]

Generalized Co-Heyting Algebra Structure on Product Types

Informal description

For any family of types $(\alpha_i)_{i \in \iota}$ where each $\alpha_i$ is a generalized co-Heyting algebra, the product type $\forall i, \alpha_i$ is also a generalized co-Heyting algebra, with the lattice operations, bottom element, and difference operation defined pointwise.

himp_bot theorem

(a : α) : a ⇨ ⊥ = aᶜ

Full source

@[simp]
theorem himp_bot (a : α) : a ⇨ ⊥ = aᶜ :=
  HeytingAlgebra.himp_bot _

Pseudo-complement as implication to bottom: $a \Rightarrow \bot = \neg a$

Informal description

For any element $a$ in a Heyting algebra $\alpha$, the Heyting implication $a \Rightarrow \bot$ is equal to the pseudo-complement $\neg a$ of $a$.

bot_himp theorem

(a : α) : ⊥ ⇨ a = ⊤

Full source

@[simp]
theorem bot_himp (a : α) : ⊥⊥ ⇨ a = ⊤ :=
  himp_eq_top_iff.2 bot_le

Implication from Bottom to Any Element is Top: $\bot \Rightarrow a = \top$

Informal description

In a Heyting algebra $\alpha$, for any element $a \in \alpha$, the Heyting implication from the bottom element $\bot$ to $a$ equals the top element $\top$, i.e., $\bot \Rightarrow a = \top$.

compl_sup_distrib theorem

(a b : α) : (a ⊔ b)ᶜ = aᶜ ⊓ bᶜ

Full source

theorem compl_sup_distrib (a b : α) : (a ⊔ b)ᶜ = aᶜaᶜ ⊓ bᶜ := by
  simp_rw [← himp_bot, sup_himp_distrib]

De Morgan's Law for Pseudo-Complements in Heyting Algebras: $\neg(a \sqcup b) = \neg a \sqcap \neg b$

Informal description

For any elements $a$ and $b$ in a Heyting algebra $\alpha$, the pseudo-complement of their join satisfies $\neg(a \sqcup b) = \neg a \sqcap \neg b$.

compl_sup theorem

: (a ⊔ b)ᶜ = aᶜ ⊓ bᶜ

Full source

@[simp]
theorem compl_sup : (a ⊔ b)ᶜ = aᶜaᶜ ⊓ bᶜ :=
  compl_sup_distrib _ _

De Morgan's Law for Pseudo-Complements in Heyting Algebras: $\neg(a \sqcup b) = \neg a \sqcap \neg b$

Informal description

For any elements $a$ and $b$ in a Heyting algebra, the pseudo-complement of their join equals the meet of their pseudo-complements, i.e., $\neg(a \sqcup b) = \neg a \sqcap \neg b$.

compl_le_himp theorem

: aᶜ ≤ a ⇨ b

Full source

theorem compl_le_himp : aᶜ ≤ a ⇨ b :=
  (himp_bot _).ge.trans <| himp_le_himp_left bot_le

Pseudo-complement is bounded by implication: $\neg a \leq (a \Rightarrow b)$

Informal description

In a Heyting algebra, the pseudo-complement $\neg a$ of an element $a$ is less than or equal to the Heyting implication $a \Rightarrow b$ for any element $b$.

compl_sup_le_himp theorem

: aᶜ ⊔ b ≤ a ⇨ b

Full source

theorem compl_sup_le_himp : aᶜaᶜ ⊔ b ≤ a ⇨ b :=
  sup_le compl_le_himp le_himp

Join of Pseudo-Complement and Element Bounds Implication: $\neg a \sqcup b \leq (a \Rightarrow b)$

Informal description

In a Heyting algebra, for any elements $a$ and $b$, the join of the pseudo-complement of $a$ (denoted $\neg a$) and $b$ is less than or equal to the Heyting implication $a \Rightarrow b$. That is, $\neg a \sqcup b \leq (a \Rightarrow b)$.

sup_compl_le_himp theorem

: b ⊔ aᶜ ≤ a ⇨ b

Full source

theorem sup_compl_le_himp : b ⊔ aᶜ ≤ a ⇨ b :=
  sup_le le_himp compl_le_himp

Join with Pseudo-Complement Bounded by Implication: $b \sqcup \neg a \leq (a \Rightarrow b)$

Informal description

For any elements $a$ and $b$ in a Heyting algebra, the join of $b$ and the pseudo-complement of $a$ is less than or equal to the Heyting implication $a \Rightarrow b$, i.e., $b \sqcup \neg a \leq (a \Rightarrow b)$.

himp_compl theorem

(a : α) : a ⇨ aᶜ = aᶜ

Full source

@[simp]
theorem himp_compl (a : α) : a ⇨ aᶜ = aᶜ := by rw [← himp_bot, himp_himp, inf_idem]

Implication of an Element with its Pseudo-Complement: $a \Rightarrow \neg a = \neg a$

Informal description

In a Heyting algebra $\alpha$, for any element $a \in \alpha$, the Heyting implication $a \Rightarrow \neg a$ equals the pseudo-complement $\neg a$.

himp_compl_comm theorem

(a b : α) : a ⇨ bᶜ = b ⇨ aᶜ

Full source

theorem himp_compl_comm (a b : α) : a ⇨ bᶜ = b ⇨ aᶜ := by simp_rw [← himp_bot, himp_left_comm]

Commutativity of Heyting Implication with Pseudo-Complement: $(a \Rightarrow \neg b) = (b \Rightarrow \neg a)$

Informal description

In a Heyting algebra $\alpha$, for any elements $a, b \in \alpha$, the Heyting implication satisfies the following commutative property with respect to the pseudo-complement: $$(a \Rightarrow \neg b) = (b \Rightarrow \neg a)$$

le_compl_iff_disjoint_right theorem

: a ≤ bᶜ ↔ Disjoint a b

Full source

theorem le_compl_iff_disjoint_right : a ≤ bᶜ ↔ Disjoint a b := by
  rw [← himp_bot, le_himp_iff, disjoint_iff_inf_le]

Pseudo-complement Characterizes Disjointness: $a \leq \neg b \leftrightarrow a \sqcap b = \bot$

Informal description

For any elements $a$ and $b$ in a Heyting algebra $\alpha$, the inequality $a \leq \neg b$ holds if and only if $a$ and $b$ are disjoint (i.e., $a \sqcap b = \bot$).

le_compl_iff_disjoint_left theorem

: a ≤ bᶜ ↔ Disjoint b a

Full source

theorem le_compl_iff_disjoint_left : a ≤ bᶜ ↔ Disjoint b a :=
  le_compl_iff_disjoint_right.trans disjoint_comm

Pseudo-complement Characterizes Disjointness (Symmetric Form): $a \leq \neg b \leftrightarrow b \sqcap a = \bot$

Informal description

For any elements $a$ and $b$ in a Heyting algebra $\alpha$, the inequality $a \leq \neg b$ holds if and only if $b$ and $a$ are disjoint (i.e., $b \sqcap a = \bot$).

le_compl_comm theorem

: a ≤ bᶜ ↔ b ≤ aᶜ

Full source

theorem le_compl_comm : a ≤ bᶜ ↔ b ≤ aᶜ := by
  rw [le_compl_iff_disjoint_right, le_compl_iff_disjoint_left]

Symmetry of Pseudo-complement Ordering: $a \leq \neg b \leftrightarrow b \leq \neg a$

Informal description

For any elements $a$ and $b$ in a Heyting algebra, the inequality $a \leq \neg b$ holds if and only if $b \leq \neg a$.

disjoint_compl_left theorem

: Disjoint aᶜ a

Full source

theorem disjoint_compl_left : Disjoint aᶜ a :=
  disjoint_iff_inf_le.mpr <| le_himp_iff.1 (himp_bot _).ge

Disjointness of Pseudo-complement: $\neg a \sqcap a = \bot$

Informal description

For any element $a$ in a Heyting algebra, the pseudo-complement $\neg a$ is disjoint from $a$, i.e., $\neg a \sqcap a = \bot$.

disjoint_compl_right theorem

: Disjoint a aᶜ

Full source

theorem disjoint_compl_right : Disjoint a aᶜ :=
  disjoint_compl_left.symm

Disjointness of Element and Pseudo-complement: $a \sqcap \neg a = \bot$

Informal description

For any element $a$ in a Heyting algebra, $a$ is disjoint from its pseudo-complement $\neg a$, i.e., $a \sqcap \neg a = \bot$.

LE.le.disjoint_compl_left theorem

(h : b ≤ a) : Disjoint aᶜ b

Full source

theorem LE.le.disjoint_compl_left (h : b ≤ a) : Disjoint aᶜ b :=
  _root_.disjoint_compl_left.mono_right h

Disjointness of Pseudo-complement Under Ordering: $b \leq a \Rightarrow \neg a \sqcap b = \bot$

Informal description

For any elements $a$ and $b$ in a Heyting algebra, if $b \leq a$, then the pseudo-complement $a^c$ is disjoint from $b$, i.e., $a^c \sqcap b = \bot$.

LE.le.disjoint_compl_right theorem

(h : a ≤ b) : Disjoint a bᶜ

Full source

theorem LE.le.disjoint_compl_right (h : a ≤ b) : Disjoint a bᶜ :=
  _root_.disjoint_compl_right.mono_left h

Disjointness Under Ordering: $a \leq b \Rightarrow a \sqcap \neg b = \bot$

Informal description

For any elements $a$ and $b$ in a Heyting algebra, if $a \leq b$, then $a$ is disjoint from the pseudo-complement of $b$, i.e., $a \sqcap \neg b = \bot$.

IsCompl.compl_eq theorem

(h : IsCompl a b) : aᶜ = b

Full source

theorem IsCompl.compl_eq (h : IsCompl a b) : aᶜ = b :=
  h.1.le_compl_left.antisymm' <| Disjoint.le_of_codisjoint disjoint_compl_left h.2

Pseudo-complement of Complement Elements in Heyting Algebra: $\neg a = b$ when $a$ and $b$ are complements

Informal description

In a Heyting algebra, if two elements $a$ and $b$ are complements (i.e., $a \sqcap b = \bot$ and $a \sqcup b = \top$), then the pseudo-complement of $a$ is equal to $b$, i.e., $\neg a = b$.

compl_unique theorem

(h₀ : a ⊓ b = ⊥) (h₁ : a ⊔ b = ⊤) : aᶜ = b

Full source

theorem compl_unique (h₀ : a ⊓ b = ⊥) (h₁ : a ⊔ b = ⊤) : aᶜ = b :=
  (IsCompl.of_eq h₀ h₁).compl_eq

Uniqueness of Pseudo-complement in Heyting Algebra: $\neg a = b$ when $a$ and $b$ are complements

Informal description

In a Heyting algebra, if two elements $a$ and $b$ satisfy $a \sqcap b = \bot$ and $a \sqcup b = \top$, then the pseudo-complement of $a$ is equal to $b$, i.e., $\neg a = b$.

inf_compl_self theorem

(a : α) : a ⊓ aᶜ = ⊥

Full source

@[simp]
theorem inf_compl_self (a : α) : a ⊓ aᶜ = ⊥ :=
  disjoint_compl_right.eq_bot

Pseudo-complement property: $a \sqcap \neg a = \bot$

Informal description

For any element $a$ in a Heyting algebra, the meet of $a$ and its pseudo-complement $a^c$ equals the bottom element, i.e., $a \sqcap a^c = \bot$.

compl_inf_self theorem

(a : α) : aᶜ ⊓ a = ⊥

Full source

@[simp]
theorem compl_inf_self (a : α) : aᶜaᶜ ⊓ a = ⊥ :=
  disjoint_compl_left.eq_bot

Pseudo-complement meets element is bottom: $a^c \sqcap a = \bot$

Informal description

For any element $a$ in a Heyting algebra, the meet (infimum) of its pseudo-complement $a^c$ and $a$ itself is equal to the bottom element $\bot$, i.e., $a^c \sqcap a = \bot$.

inf_compl_eq_bot theorem

: a ⊓ aᶜ = ⊥

Full source

theorem inf_compl_eq_bot : a ⊓ aᶜ = ⊥ :=
  inf_compl_self _

Pseudo-complement property: $a \sqcap \neg a = \bot$

Informal description

For any element $a$ in a Heyting algebra, the meet (infimum) of $a$ and its pseudo-complement $\neg a$ equals the bottom element $\bot$, i.e., $a \sqcap \neg a = \bot$.

compl_inf_eq_bot theorem

: aᶜ ⊓ a = ⊥

Full source

theorem compl_inf_eq_bot : aᶜaᶜ ⊓ a = ⊥ :=
  compl_inf_self _

Pseudo-complement meets element is bottom: $a^c \sqcap a = \bot$

Informal description

For any element $a$ in a Heyting algebra, the meet (infimum) of its pseudo-complement $a^c$ and $a$ itself is equal to the bottom element $\bot$, i.e., $a^c \sqcap a = \bot$.

compl_top theorem

: (⊤ : α)ᶜ = ⊥

Full source

@[simp]
theorem compl_top : (⊤ : α)ᶜ = ⊥ :=
  eq_of_forall_le_iff fun a => by rw [le_compl_iff_disjoint_right, disjoint_top, le_bot_iff]

Pseudo-complement of Top is Bottom: $\neg \top = \bot$

Informal description

In a Heyting algebra $\alpha$, the pseudo-complement of the top element $\top$ is equal to the bottom element $\bot$, i.e., $\neg \top = \bot$.

compl_bot theorem

: (⊥ : α)ᶜ = ⊤

Full source

@[simp]
theorem compl_bot : (⊥ : α)ᶜ = ⊤ := by rw [← himp_bot, himp_self]

Pseudo-complement of Bottom is Top: $\neg \bot = \top$

Informal description

In a Heyting algebra $\alpha$, the pseudo-complement of the bottom element $\bot$ is equal to the top element $\top$, i.e., $\neg \bot = \top$.

le_compl_self theorem

: a ≤ aᶜ ↔ a = ⊥

Full source

@[simp] theorem le_compl_self : a ≤ aᶜ ↔ a = ⊥ := by
  rw [le_compl_iff_disjoint_left, disjoint_self]

Characterization of Bottom Element via Pseudo-complement: $a \leq \neg a \leftrightarrow a = \bot$

Informal description

For any element $a$ in a Heyting algebra $\alpha$, the inequality $a \leq \neg a$ holds if and only if $a$ is equal to the bottom element $\bot$.

ne_compl_self theorem

[Nontrivial α] : a ≠ aᶜ

Full source

@[simp] theorem ne_compl_self [Nontrivial α] : a ≠ aᶜ := by
  intro h
  cases le_compl_self.1 (le_of_eq h)
  simp at h

Non-identity of Element and its Pseudo-complement in Nontrivial Heyting Algebra

Informal description

In a nontrivial Heyting algebra $\alpha$, for any element $a \in \alpha$, the element $a$ is not equal to its pseudo-complement $\neg a$.

compl_ne_self theorem

[Nontrivial α] : aᶜ ≠ a

Full source

@[simp] theorem compl_ne_self [Nontrivial α] : aᶜaᶜ ≠ a :=
  ne_comm.1 ne_compl_self

Non-identity of Pseudo-complement and Element in Nontrivial Heyting Algebra

Informal description

In a nontrivial Heyting algebra $\alpha$, for any element $a \in \alpha$, the pseudo-complement $\neg a$ is not equal to $a$.

lt_compl_self theorem

[Nontrivial α] : a < aᶜ ↔ a = ⊥

Full source

@[simp] theorem lt_compl_self [Nontrivial α] : a < aᶜ ↔ a = ⊥ := by
  rw [lt_iff_le_and_ne]; simp

Characterization of Bottom Element via Pseudo-Complement in Heyting Algebra

Informal description

In a nontrivial Heyting algebra $\alpha$, for any element $a \in \alpha$, the strict inequality $a < \neg a$ holds if and only if $a$ is the bottom element $\bot$.

le_compl_compl theorem

: a ≤ aᶜᶜ

Full source

theorem le_compl_compl : a ≤ aᶜaᶜᶜ :=
  disjoint_compl_right.le_compl_right

Double Pseudo-Complement Inequality in Heyting Algebra: $a \leq \neg \neg a$

Informal description

For any element $a$ in a Heyting algebra, $a$ is less than or equal to the double pseudo-complement of $a$, i.e., $a \leq \neg \neg a$.

compl_anti theorem

: Antitone (compl : α → α)

Full source

theorem compl_anti : Antitone (compl : α → α) := fun _ _ h =>
  le_compl_comm.1 <| h.trans le_compl_compl

Antitonicity of Pseudo-Complement in Heyting Algebra

Informal description

The pseudo-complement operation $\neg$ in a Heyting algebra is antitone, meaning that for any elements $a, b \in \alpha$, if $a \leq b$ then $\neg b \leq \neg a$.

compl_le_compl theorem

(h : a ≤ b) : bᶜ ≤ aᶜ

Full source

@[gcongr]
theorem compl_le_compl (h : a ≤ b) : bᶜ ≤ aᶜ :=
  compl_anti h

Pseudo-complement reverses order: $a \leq b \implies \neg b \leq \neg a$

Informal description

For any elements $a$ and $b$ in a Heyting algebra, if $a \leq b$, then the pseudo-complement of $b$ is less than or equal to the pseudo-complement of $a$, i.e., $\neg b \leq \neg a$.

compl_compl_compl theorem

(a : α) : aᶜᶜᶜ = aᶜ

Full source

@[simp]
theorem compl_compl_compl (a : α) : aᶜaᶜᶜaᶜᶜᶜ = aᶜ :=
  (compl_anti le_compl_compl).antisymm le_compl_compl

Triple Pseudo-Complement Identity: $\neg \neg \neg a = \neg a$ in Heyting Algebra

Informal description

For any element $a$ in a Heyting algebra, the triple pseudo-complement of $a$ is equal to the pseudo-complement of $a$, i.e., $\neg \neg \neg a = \neg a$.

disjoint_compl_compl_left_iff theorem

: Disjoint aᶜᶜ b ↔ Disjoint a b

Full source

@[simp]
theorem disjoint_compl_compl_left_iff : DisjointDisjoint aᶜᶜ b ↔ Disjoint a b := by
  simp_rw [← le_compl_iff_disjoint_left, compl_compl_compl]

Double Negation Preserves Disjointness: $\neg\neg a \perp b \iff a \perp b$

Informal description

For any elements $a$ and $b$ in a Heyting algebra, the elements $\neg \neg a$ and $b$ are disjoint if and only if $a$ and $b$ are disjoint. In other words, $\neg \neg a \sqcap b = \bot$ holds precisely when $a \sqcap b = \bot$.

disjoint_compl_compl_right_iff theorem

: Disjoint a bᶜᶜ ↔ Disjoint a b

Full source

@[simp]
theorem disjoint_compl_compl_right_iff : DisjointDisjoint a bᶜᶜ ↔ Disjoint a b := by
  simp_rw [← le_compl_iff_disjoint_right, compl_compl_compl]

Disjointness with Double Pseudo-Complement is Equivalent to Original Disjointness

Informal description

For any elements $a$ and $b$ in a Heyting algebra, $a$ is disjoint from the double pseudo-complement of $b$ if and only if $a$ is disjoint from $b$ itself. In symbols: $$a \sqcap \neg\neg b = \bot \iff a \sqcap b = \bot$$

compl_sup_compl_le theorem

: aᶜ ⊔ bᶜ ≤ (a ⊓ b)ᶜ

Full source

theorem compl_sup_compl_le : aᶜaᶜ ⊔ bᶜ ≤ (a ⊓ b)ᶜ :=
  sup_le (compl_anti inf_le_left) <| compl_anti inf_le_right

Pseudo-complement Inequality: $a^c \sqcup b^c \leq (a \sqcap b)^c$

Informal description

In a Heyting algebra, for any elements $a$ and $b$, the join of their pseudo-complements $a^c \sqcup b^c$ is less than or equal to the pseudo-complement of their meet $(a \sqcap b)^c$. That is, $a^c \sqcup b^c \leq (a \sqcap b)^c$.

compl_compl_inf_distrib theorem

(a b : α) : (a ⊓ b)ᶜᶜ = aᶜᶜ ⊓ bᶜᶜ

Full source

theorem compl_compl_inf_distrib (a b : α) : (a ⊓ b)ᶜ(a ⊓ b)ᶜᶜ = aᶜaᶜᶜaᶜᶜ ⊓ bᶜᶜ := by
  refine ((compl_anti compl_sup_compl_le).trans (compl_sup_distrib _ _).le).antisymm ?_
  rw [le_compl_iff_disjoint_right, disjoint_assoc, disjoint_compl_compl_left_iff,
    disjoint_left_comm, disjoint_compl_compl_left_iff, ← disjoint_assoc, inf_comm]
  exact disjoint_compl_right

Double Negation Distributes Over Meet in Heyting Algebras: $\neg\neg(a \sqcap b) = \neg\neg a \sqcap \neg\neg b$

Informal description

For any elements $a$ and $b$ in a Heyting algebra $\alpha$, the double pseudo-complement of their meet equals the meet of their double pseudo-complements. That is: $$ \neg\neg(a \sqcap b) = \neg\neg a \sqcap \neg\neg b $$

compl_compl_himp_distrib theorem

(a b : α) : (a ⇨ b)ᶜᶜ = aᶜᶜ ⇨ bᶜᶜ

Full source

theorem compl_compl_himp_distrib (a b : α) : (a ⇨ b)ᶜ(a ⇨ b)ᶜᶜ = aᶜaᶜᶜaᶜᶜ ⇨ bᶜᶜ := by
  apply le_antisymm
  · rw [le_himp_iff, ← compl_compl_inf_distrib]
    exact compl_anti (compl_anti himp_inf_le)
  · refine le_compl_comm.1 ((compl_anti compl_sup_le_himp).trans ?_)
    rw [compl_sup_distrib, le_compl_iff_disjoint_right, disjoint_right_comm, ←
      le_compl_iff_disjoint_right]
    exact inf_himp_le

Double Negation Distributes Over Heyting Implication: $\neg\neg(a \Rightarrow b) = \neg\neg a \Rightarrow \neg\neg b$

Informal description

For any elements $a$ and $b$ in a Heyting algebra $\alpha$, the double pseudo-complement of the Heyting implication $a \Rightarrow b$ equals the Heyting implication of the double pseudo-complements of $a$ and $b$. That is: $$ \neg\neg(a \Rightarrow b) = \neg\neg a \Rightarrow \neg\neg b $$

OrderDual.instCoheytingAlgebra instance

: CoheytingAlgebra αᵒᵈ

Full source

instance OrderDual.instCoheytingAlgebra : CoheytingAlgebra αᵒᵈ where
  hnot := toDualtoDual ∘ compl ∘ ofDual
  sdiff a b := toDual (ofDualofDual b ⇨ ofDual a)
  sdiff_le_iff a b c := by rw [sup_comm]; exact le_himp_iff
  top_sdiff := @himp_bot α _

Order Dual of a Heyting Algebra is a Co-Heyting Algebra

Informal description

The order dual $\alpha^{\text{op}}$ of any Heyting algebra $\alpha$ forms a co-Heyting algebra, where the operations are defined dually. Specifically: - The difference operation $a \setminus b$ in $\alpha^{\text{op}}$ corresponds to the Heyting implication $b \Rightarrow a$ in $\alpha$. - The negation $\neg a$ in $\alpha^{\text{op}}$ corresponds to the pseudo-complement $\neg a$ in $\alpha$. - The top and bottom elements are swapped.

ofDual_hnot theorem

(a : αᵒᵈ) : ofDual (￢a) = (ofDual a)ᶜ

Full source

@[simp]
theorem ofDual_hnot (a : αᵒᵈ) : ofDual (￢a) = (ofDual a)ᶜ :=
  rfl

Negation in Order Dual Corresponds to Pseudo-Complement in Heyting Algebra

Informal description

For any element $a$ in the order dual $\alpha^{\text{op}}$ of a Heyting algebra $\alpha$, the negation $\neg a$ in $\alpha^{\text{op}}$ corresponds to the pseudo-complement $(a)^\complement$ in $\alpha$ when mapped back via the order duality isomorphism.

toDual_compl theorem

(a : α) : toDual aᶜ = ￢toDual a

Full source

@[simp]
theorem toDual_compl (a : α) : toDual aᶜ = ￢toDual a :=
  rfl

Dual Pseudo-Complement Equals Negation of Dual

Informal description

For any element $a$ in a Heyting algebra $\alpha$, the pseudo-complement of $a$ in the order dual $\alpha^{\text{op}}$ is equal to the negation of the dual element of $a$. In symbols, this means: \[ \text{toDual}(a^\complement) = \neg \text{toDual}(a) \] where $\text{toDual} : \alpha \to \alpha^{\text{op}}$ is the canonical map sending an element to its order dual, $(\cdot)^\complement$ is the pseudo-complement operation in $\alpha$, and $\neg$ is the negation operation in $\alpha^{\text{op}}$.

Prod.instHeytingAlgebra instance

[HeytingAlgebra β] : HeytingAlgebra (α × β)

Full source

instance Prod.instHeytingAlgebra [HeytingAlgebra β] : HeytingAlgebra (α × β) where
    himp_bot a := Prod.ext_iff.2 ⟨himp_bot a.1, himp_bot a.2⟩

Heyting Algebra Structure on Product Types

Informal description

For any two Heyting algebras $\alpha$ and $\beta$, the product $\alpha \times \beta$ is also a Heyting algebra, with the Heyting implication, pseudo-complement, and order structure defined componentwise. Specifically: 1. The Heyting implication is given by $(a_1, b_1) \Rightarrow (a_2, b_2) = (a_1 \Rightarrow a_2, b_1 \Rightarrow b_2)$ 2. The pseudo-complement is given by $\neg (a, b) = (\neg a, \neg b)$ 3. The order is given by $(a_1, b_1) \leq (a_2, b_2)$ if and only if $a_1 \leq a_2$ and $b_1 \leq b_2$ 4. The bottom element is $(\bot, \bot)$ and the top element is $(\top, \top)$

Pi.instHeytingAlgebra instance

{α : ι → Type*} [∀ i, HeytingAlgebra (α i)] : HeytingAlgebra (∀ i, α i)

Full source

instance Pi.instHeytingAlgebra {α : ι → Type*} [∀ i, HeytingAlgebra (α i)] :
    HeytingAlgebra (∀ i, α i) where
  himp_bot f := funext fun i ↦ himp_bot (f i)

Pointwise Heyting Algebra Structure on Product Types

Informal description

For any family of Heyting algebras $(\alpha_i)_{i \in \iota}$, the product type $\forall i, \alpha_i$ is also a Heyting algebra, with the Heyting implication, pseudo-complement, and order structure defined pointwise. Specifically: 1. The Heyting implication is given by $(f \Rightarrow g)(i) = f(i) \Rightarrow g(i)$ for all $i \in \iota$, 2. The pseudo-complement is given by $(\neg f)(i) = \neg f(i)$ for all $i \in \iota$, 3. The order is given by $f \leq g$ if and only if $f(i) \leq g(i)$ for all $i \in \iota$, 4. The bottom element is the function that returns $\bot$ for every $i \in \iota$, 5. The top element is the function that returns $\top$ for every $i \in \iota$.

top_sdiff' theorem

(a : α) : ⊤ \ a = ￢a

Full source

@[simp]
theorem top_sdiff' (a : α) : ⊤⊤ \ a = ￢a :=
  CoheytingAlgebra.top_sdiff _

Top Difference Equals Negation in Co-Heyting Algebra

Informal description

In a co-Heyting algebra $\alpha$, for any element $a \in \alpha$, the difference between the top element $\top$ and $a$ equals the negation of $a$, i.e., $\top \setminus a = \neg a$.

sdiff_top theorem

(a : α) : a \ ⊤ = ⊥

Full source

@[simp]
theorem sdiff_top (a : α) : a \ ⊤ = ⊥ :=
  sdiff_eq_bot_iff.2 le_top

Difference with Top is Bottom: $a \setminus \top = \bot$

Informal description

For any element $a$ in a co-Heyting algebra $\alpha$, the difference $a \setminus \top$ equals the bottom element $\bot$.

hnot_inf_distrib theorem

(a b : α) : ￢(a ⊓ b) = ￢a ⊔ ￢b

Full source

theorem hnot_inf_distrib (a b : α) : ￢(a ⊓ b) = ￢a￢a ⊔ ￢b := by
  simp_rw [← top_sdiff', sdiff_inf_distrib]

De Morgan's Law for Negation in Co-Heyting Algebras: $\neg(a \sqcap b) = \neg a \sqcup \neg b$

Informal description

In a co-Heyting algebra $\alpha$, for any elements $a, b \in \alpha$, the negation of the meet of $a$ and $b$ equals the join of their negations, i.e., $$\neg(a \sqcap b) = \neg a \sqcup \neg b.$$

sdiff_le_hnot theorem

: a \ b ≤ ￢b

Full source

theorem sdiff_le_hnot : a \ b ≤ ￢b :=
  (sdiff_le_sdiff_right le_top).trans_eq <| top_sdiff' _

Difference is Bounded by Negation in Co-Heyting Algebra

Informal description

In a co-Heyting algebra, for any elements $a$ and $b$, the difference $a \setminus b$ is less than or equal to the negation of $b$, i.e., $a \setminus b \leq \neg b$.

sdiff_le_inf_hnot theorem

: a \ b ≤ a ⊓ ￢b

Full source

theorem sdiff_le_inf_hnot : a \ b ≤ a ⊓ ￢b :=
  le_inf sdiff_le sdiff_le_hnot

Difference Bounded by Meet with Negation in Co-Heyting Algebra

Informal description

In a co-Heyting algebra, for any elements $a$ and $b$, the difference $a \setminus b$ is less than or equal to both $a$ and the negation of $b$, i.e., $a \setminus b \leq a \sqcap \neg b$.

CoheytingAlgebra.toDistribLattice instance

: DistribLattice α

Full source

instance (priority := 100) CoheytingAlgebra.toDistribLattice : DistribLattice α :=
  { ‹CoheytingAlgebra α› with
    le_sup_inf :=
      fun a b c => by simp_rw [← sdiff_le_iff, le_inf_iff, sdiff_le_iff, ← le_inf_iff]; rfl }

Co-Heyting Algebras are Distributive Lattices

Informal description

Every co-Heyting algebra is a distributive lattice.

hnot_sdiff theorem

(a : α) : ￢a \ a = ￢a

Full source

@[simp]
theorem hnot_sdiff (a : α) : ￢a￢a \ a = ￢a := by rw [← top_sdiff', sdiff_sdiff, sup_idem]

Negation Difference Identity in Co-Heyting Algebra: $\neg a \setminus a = \neg a$

Informal description

In a co-Heyting algebra $\alpha$, for any element $a \in \alpha$, the difference between the negation of $a$ and $a$ itself equals the negation of $a$, i.e., $\neg a \setminus a = \neg a$.

hnot_sdiff_comm theorem

(a b : α) : ￢a \ b = ￢b \ a

Full source

theorem hnot_sdiff_comm (a b : α) : ￢a￢a \ b = ￢b￢b \ a := by simp_rw [← top_sdiff', sdiff_right_comm]

Commutativity of Negation and Difference in Co-Heyting Algebra

Informal description

In a co-Heyting algebra $\alpha$, for any elements $a, b \in \alpha$, the difference of the negation of $a$ and $b$ equals the difference of the negation of $b$ and $a$, i.e., $\neg a \setminus b = \neg b \setminus a$.

hnot_le_iff_codisjoint_right theorem

: ￢a ≤ b ↔ Codisjoint a b

Full source

theorem hnot_le_iff_codisjoint_right : ￢a￢a ≤ b ↔ Codisjoint a b := by
  rw [← top_sdiff', sdiff_le_iff, codisjoint_iff_le_sup]

Negation Bound by Codisjointness: $\neg a \leq b \leftrightarrow a \sqcup b = \top$

Informal description

In a co-Heyting algebra, the negation $\neg a$ of an element $a$ is less than or equal to an element $b$ if and only if $a$ and $b$ are codisjoint (i.e., $a \sqcup b = \top$).

hnot_le_iff_codisjoint_left theorem

: ￢a ≤ b ↔ Codisjoint b a

Full source

theorem hnot_le_iff_codisjoint_left : ￢a￢a ≤ b ↔ Codisjoint b a :=
  hnot_le_iff_codisjoint_right.trans codisjoint_comm

Negation Bound by Codisjointness (Symmetric Form): $\neg a \leq b \leftrightarrow b \sqcup a = \top$

Informal description

In a co-Heyting algebra, the negation $\neg a$ of an element $a$ is less than or equal to an element $b$ if and only if $b$ and $a$ are codisjoint (i.e., $b \sqcup a = \top$).

hnot_le_comm theorem

: ￢a ≤ b ↔ ￢b ≤ a

Full source

theorem hnot_le_comm : ￢a￢a ≤ b ↔ ￢b ≤ a := by
  rw [hnot_le_iff_codisjoint_right, hnot_le_iff_codisjoint_left]

Negation Order Commutation in Co-Heyting Algebra: $\neg a \leq b \leftrightarrow \neg b \leq a$

Informal description

In a co-Heyting algebra, the negation $\neg a$ of an element $a$ is less than or equal to an element $b$ if and only if the negation $\neg b$ is less than or equal to $a$. That is, $\neg a \leq b \leftrightarrow \neg b \leq a$.

codisjoint_hnot_right theorem

: Codisjoint a (￢a)

Full source

theorem codisjoint_hnot_right : Codisjoint a (￢a) :=
  codisjoint_iff_le_sup.2 <| sdiff_le_iff.1 (top_sdiff' _).le

Codisjointness of an Element and its Negation in a Co-Heyting Algebra

Informal description

In a co-Heyting algebra, for any element $a$, the element $a$ and its negation $\neg a$ are codisjoint, i.e., $a \sqcup \neg a = \top$.

codisjoint_hnot_left theorem

: Codisjoint (￢a) a

Full source

theorem codisjoint_hnot_left : Codisjoint (￢a) a :=
  codisjoint_hnot_right.symm

Codisjointness of Negation and Element in Co-Heyting Algebra

Informal description

In a co-Heyting algebra, for any element $a$, the negation $\neg a$ and the element $a$ are codisjoint, i.e., $\neg a \sqcup a = \top$.

LE.le.codisjoint_hnot_left theorem

(h : a ≤ b) : Codisjoint (￢a) b

Full source

theorem LE.le.codisjoint_hnot_left (h : a ≤ b) : Codisjoint (￢a) b :=
  _root_.codisjoint_hnot_left.mono_right h

Codisjointness of Negation and Larger Element: $\neg a \sqcup b = \top$ when $a \leq b$

Informal description

In a co-Heyting algebra, if $a \leq b$, then the negation $\neg a$ and $b$ are codisjoint, i.e., $\neg a \sqcup b = \top$.

LE.le.codisjoint_hnot_right theorem

(h : b ≤ a) : Codisjoint a (￢b)

Full source

theorem LE.le.codisjoint_hnot_right (h : b ≤ a) : Codisjoint a (￢b) :=
  _root_.codisjoint_hnot_right.mono_left h

Codisjointness of Element and Negation Under Ordering in Co-Heyting Algebra

Informal description

In a co-Heyting algebra, for any elements $a$ and $b$ such that $b \leq a$, the element $a$ and the negation of $b$ (denoted $\neg b$) are codisjoint, i.e., $a \sqcup \neg b = \top$.

IsCompl.hnot_eq theorem

(h : IsCompl a b) : ￢a = b

Full source

theorem IsCompl.hnot_eq (h : IsCompl a b) : ￢a = b :=
  h.2.hnot_le_right.antisymm <| Disjoint.le_of_codisjoint h.1.symm codisjoint_hnot_right

Negation of Complement in Co-Heyting Algebra: $\neg a = b$ when $a$ and $b$ are complements

Informal description

In a co-Heyting algebra, if two elements $a$ and $b$ are complements (i.e., $a \sqcap b = \bot$ and $a \sqcup b = \top$), then the negation of $a$ is equal to $b$, i.e., $\neg a = b$.

sup_hnot_self theorem

(a : α) : a ⊔ ￢a = ⊤

Full source

@[simp]
theorem sup_hnot_self (a : α) : a ⊔ ￢a = ⊤ :=
  Codisjoint.eq_top codisjoint_hnot_right

Join of Element and its Negation is Top in Co-Heyting Algebra

Informal description

In a co-Heyting algebra $\alpha$, for any element $a \in \alpha$, the join of $a$ and its negation $\neg a$ equals the top element $\top$, i.e., $a \sqcup \neg a = \top$.

hnot_sup_self theorem

(a : α) : ￢a ⊔ a = ⊤

Full source

@[simp]
theorem hnot_sup_self (a : α) : ￢a￢a ⊔ a = ⊤ :=
  Codisjoint.eq_top codisjoint_hnot_left

Join of Negation and Element is Top in Co-Heyting Algebra

Informal description

In a co-Heyting algebra $\alpha$, for any element $a \in \alpha$, the join of the negation $\neg a$ and $a$ equals the top element $\top$, i.e., $\neg a \sqcup a = \top$.

hnot_bot theorem

: ￢(⊥ : α) = ⊤

Full source

@[simp]
theorem hnot_bot : ￢(⊥ : α) = ⊤ :=
  eq_of_forall_ge_iff fun a => by rw [hnot_le_iff_codisjoint_left, codisjoint_bot, top_le_iff]

Negation of Bottom is Top in Co-Heyting Algebra

Informal description

In a co-Heyting algebra $\alpha$, the negation of the bottom element $\bot$ equals the top element $\top$, i.e., $\neg \bot = \top$.

hnot_top theorem

: ￢(⊤ : α) = ⊥

Full source

@[simp]
theorem hnot_top : ￢(⊤ : α) = ⊥ := by rw [← top_sdiff', sdiff_self]

Negation of Top is Bottom in Co-Heyting Algebra

Informal description

In a co-Heyting algebra $\alpha$, the negation of the top element $\top$ equals the bottom element $\bot$, i.e., $\neg \top = \bot$.

hnot_hnot_le theorem

: ￢￢a ≤ a

Full source

theorem hnot_hnot_le : ￢￢a ≤ a :=
  codisjoint_hnot_right.hnot_le_left

Double Negation Inequality in Co-Heyting Algebra

Informal description

In a co-Heyting algebra, for any element $a$, the double negation of $a$ is less than or equal to $a$, i.e., $\neg \neg a \leq a$.

hnot_anti theorem

: Antitone (hnot : α → α)

Full source

theorem hnot_anti : Antitone (hnot : α → α) := fun _ _ h => hnot_le_comm.1 <| hnot_hnot_le.trans h

Antitonicity of Negation in Co-Heyting Algebra

Informal description

The negation operation $\neg$ in a co-Heyting algebra $\alpha$ is antitone, meaning that for any elements $a, b \in \alpha$, if $a \leq b$, then $\neg b \leq \neg a$.

hnot_le_hnot theorem

(h : a ≤ b) : ￢b ≤ ￢a

Full source

theorem hnot_le_hnot (h : a ≤ b) : ￢b ≤ ￢a :=
  hnot_anti h

Antitonicity of Negation in Co-Heyting Algebra

Informal description

In a co-Heyting algebra, if $a \leq b$, then $\neg b \leq \neg a$.

hnot_hnot_hnot theorem

(a : α) : ￢￢￢a = ￢a

Full source

@[simp]
theorem hnot_hnot_hnot (a : α) : ￢￢￢a = ￢a :=
  hnot_hnot_le.antisymm <| hnot_anti hnot_hnot_le

Triple Negation Identity in Co-Heyting Algebra

Informal description

In a co-Heyting algebra $\alpha$, for any element $a \in \alpha$, the triple negation of $a$ is equal to the negation of $a$, i.e., $\neg \neg \neg a = \neg a$.

codisjoint_hnot_hnot_left_iff theorem

: Codisjoint (￢￢a) b ↔ Codisjoint a b

Full source

@[simp]
theorem codisjoint_hnot_hnot_left_iff : CodisjointCodisjoint (￢￢a) b ↔ Codisjoint a b := by
  simp_rw [← hnot_le_iff_codisjoint_right, hnot_hnot_hnot]

Codisjointness Invariance under Double Negation

Informal description

In a co-Heyting algebra $\alpha$, for any elements $a, b \in \alpha$, the double negation of $a$ is codisjoint with $b$ if and only if $a$ is codisjoint with $b$. That is, $\text{Codisjoint}(\neg\neg a, b) \leftrightarrow \text{Codisjoint}(a, b)$, where codisjointness means that $\neg\neg a \sqcup b = \top$.

codisjoint_hnot_hnot_right_iff theorem

: Codisjoint a (￢￢b) ↔ Codisjoint a b

Full source

@[simp]
theorem codisjoint_hnot_hnot_right_iff : CodisjointCodisjoint a (￢￢b) ↔ Codisjoint a b := by
  simp_rw [← hnot_le_iff_codisjoint_left, hnot_hnot_hnot]

Codisjointness Invariance Under Double Negation on Right Argument

Informal description

For any elements $a$ and $b$ in a co-Heyting algebra $\alpha$, the elements $a$ and $\neg\neg b$ are codisjoint if and only if $a$ and $b$ are codisjoint. Here, two elements $x$ and $y$ are called codisjoint if $x \sqcup y = \top$.

le_hnot_inf_hnot theorem

: ￢(a ⊔ b) ≤ ￢a ⊓ ￢b

Full source

theorem le_hnot_inf_hnot : ￢(a ⊔ b) ≤ ￢a￢a ⊓ ￢b :=
  le_inf (hnot_anti le_sup_left) <| hnot_anti le_sup_right

Negation of Join is Bounded by Meet of Negations in Co-Heyting Algebra

Informal description

In a co-Heyting algebra $\alpha$, for any elements $a, b \in \alpha$, the negation of the join $a \sqcup b$ is less than or equal to the meet of the negations of $a$ and $b$, i.e., $\neg(a \sqcup b) \leq \neg a \sqcap \neg b$.

hnot_hnot_sup_distrib theorem

(a b : α) : ￢￢(a ⊔ b) = ￢￢a ⊔ ￢￢b

Full source

theorem hnot_hnot_sup_distrib (a b : α) : ￢￢(a ⊔ b) = ￢￢a￢￢a ⊔ ￢￢b := by
  refine ((hnot_inf_distrib _ _).ge.trans <| hnot_anti le_hnot_inf_hnot).antisymm' ?_
  rw [hnot_le_iff_codisjoint_left, codisjoint_assoc, codisjoint_hnot_hnot_left_iff,
    codisjoint_left_comm, codisjoint_hnot_hnot_left_iff, ← codisjoint_assoc, sup_comm]
  exact codisjoint_hnot_right

Double Negation Distributes Over Join in Co-Heyting Algebras

Informal description

In a co-Heyting algebra $\alpha$, for any elements $a, b \in \alpha$, the double negation of the join $a \sqcup b$ equals the join of the double negations of $a$ and $b$. That is, $$\neg\neg(a \sqcup b) = \neg\neg a \sqcup \neg\neg b.$$

hnot_hnot_sdiff_distrib theorem

(a b : α) : ￢￢(a \ b) = ￢￢a \ ￢￢b

Full source

theorem hnot_hnot_sdiff_distrib (a b : α) : ￢￢(a \ b) = ￢￢a￢￢a \ ￢￢b := by
  apply le_antisymm
  · refine hnot_le_comm.1 ((hnot_anti sdiff_le_inf_hnot).trans' ?_)
    rw [hnot_inf_distrib, hnot_le_iff_codisjoint_right, codisjoint_left_comm, ←
      hnot_le_iff_codisjoint_right]
    exact le_sdiff_sup
  · rw [sdiff_le_iff, ← hnot_hnot_sup_distrib]
    exact hnot_anti (hnot_anti le_sup_sdiff)

Double Negation Distributes Over Difference in Co-Heyting Algebras: $\neg\neg(a \setminus b) = \neg\neg a \setminus \neg\neg b$

Informal description

In a co-Heyting algebra $\alpha$, for any elements $a, b \in \alpha$, the double negation of the difference $a \setminus b$ equals the difference of the double negations of $a$ and $b$. That is, $$\neg\neg(a \setminus b) = \neg\neg a \setminus \neg\neg b.$$

OrderDual.instHeytingAlgebra instance

: HeytingAlgebra αᵒᵈ

Full source

instance OrderDual.instHeytingAlgebra : HeytingAlgebra αᵒᵈ where
  compl := toDualtoDual ∘ hnot ∘ ofDual
  himp a b := toDual (ofDualofDual b \ ofDual a)
  le_himp_iff a b c := by rw [inf_comm]; exact sdiff_le_iff
  himp_bot := @top_sdiff' α _

Order Dual of a Heyting Algebra is a Heyting Algebra

Informal description

For any Heyting algebra $\alpha$, the order dual $\alpha^{\text{op}}$ is also a Heyting algebra, where the implication operation is given by $a \Rightarrow b = b \setminus a$ and the pseudo-complement is given by $\neg a$.

ofDual_compl theorem

(a : αᵒᵈ) : ofDual aᶜ = ￢ofDual a

Full source

@[simp]
theorem ofDual_compl (a : αᵒᵈ) : ofDual aᶜ = ￢ofDual a :=
  rfl

Pseudo-complement in Order Dual Equals Negation in Original Co-Heyting Algebra

Informal description

For any element $a$ in the order dual $\alpha^{\text{op}}$ of a co-Heyting algebra $\alpha$, the pseudo-complement of $a$ in the dual algebra equals the negation of $a$ in the original algebra, i.e., $\text{ofDual}(a^\complement) = \neg \text{ofDual}(a)$.

ofDual_himp theorem

(a b : αᵒᵈ) : ofDual (a ⇨ b) = ofDual b \ ofDual a

Full source

@[simp]
theorem ofDual_himp (a b : αᵒᵈ) : ofDual (a ⇨ b) = ofDualofDual b \ ofDual a :=
  rfl

Dual Implication to Difference: $\text{ofDual}(a \Rightarrow b) = \text{ofDual}(b) \setminus \text{ofDual}(a)$

Informal description

For any elements $a$ and $b$ in the order dual $\alpha^{\text{op}}$ of a co-Heyting algebra $\alpha$, the Heyting implication $a \Rightarrow b$ in $\alpha^{\text{op}}$ corresponds to the difference operation $\text{ofDual}(b) \setminus \text{ofDual}(a)$ in $\alpha$. In other words, the map $\text{ofDual}$ converts the Heyting implication in the dual algebra to the difference operation in the original algebra.

toDual_hnot theorem

(a : α) : toDual (￢a) = (toDual a)ᶜ

Full source

@[simp]
theorem toDual_hnot (a : α) : toDual (￢a) = (toDual a)ᶜ :=
  rfl

Duality of Negation in Co-Heyting Algebras: $\text{toDual}(\neg a) = (\text{toDual}(a))^c$

Informal description

For any element $a$ in a co-Heyting algebra $\alpha$, the order dual of the negation $\neg a$ is equal to the complement of the order dual of $a$ in the Heyting algebra $\alpha^{\text{op}}$. In symbols, this is expressed as $\text{toDual}(\neg a) = (\text{toDual}(a))^c$.

toDual_sdiff theorem

(a b : α) : toDual (a \ b) = toDual b ⇨ toDual a

Full source

@[simp]
theorem toDual_sdiff (a b : α) : toDual (a \ b) = toDualtoDual b ⇨ toDual a :=
  rfl

Dual of Difference in Co-Heyting Algebra Equals Implication of Duals

Informal description

For any elements $a$ and $b$ in a co-Heyting algebra $\alpha$, the order dual of the difference $a \setminus b$ is equal to the Heyting implication of the order dual of $b$ and the order dual of $a$, i.e., $\text{toDual}(a \setminus b) = \text{toDual}(b) \Rightarrow \text{toDual}(a)$.

Prod.instCoheytingAlgebra instance

[CoheytingAlgebra β] : CoheytingAlgebra (α × β)

Full source

instance Prod.instCoheytingAlgebra [CoheytingAlgebra β] : CoheytingAlgebra (α × β) where
  sdiff_le_iff _ _ _ := and_congr sdiff_le_iff sdiff_le_iff
  top_sdiff a := Prod.ext_iff.2 ⟨top_sdiff' a.1, top_sdiff' a.2⟩

Product of Co-Heyting Algebras is a Co-Heyting Algebra

Informal description

For any two co-Heyting algebras $\alpha$ and $\beta$, the product type $\alpha \times \beta$ is also a co-Heyting algebra, where all operations (including the difference $\setminus$, negation $\neg$, join $\sqcup$, meet $\sqcap$, top $\top$, and bottom $\bot$) are defined componentwise.

Pi.instCoheytingAlgebra instance

{α : ι → Type*} [∀ i, CoheytingAlgebra (α i)] : CoheytingAlgebra (∀ i, α i)

Full source

instance Pi.instCoheytingAlgebra {α : ι → Type*} [∀ i, CoheytingAlgebra (α i)] :
    CoheytingAlgebra (∀ i, α i) where
  top_sdiff f := funext fun i ↦ top_sdiff' (f i)

Pointwise Co-Heyting Algebra Structure on Product Types

Informal description

For any family of types $(\alpha_i)_{i \in \iota}$ where each $\alpha_i$ is a co-Heyting algebra, the product type $\forall i, \alpha_i$ is also a co-Heyting algebra, with the lattice operations, difference operation, negation, and top element defined pointwise.

compl_le_hnot theorem

: aᶜ ≤ ￢a

Full source

theorem compl_le_hnot : aᶜ ≤ ￢a :=
  (disjoint_compl_left : Disjoint _ a).le_of_codisjoint codisjoint_hnot_right

Pseudo-complement is Weaker Than Negation in Bi-Heyting Algebras

Informal description

In a bi-Heyting algebra, the pseudo-complement $a^c$ of any element $a$ is less than or equal to its negation $\neg a$.

Prop.instHeytingAlgebra instance

: HeytingAlgebra Prop

Full source

/-- Propositions form a Heyting algebra with implication as Heyting implication and negation as
complement. -/
instance Prop.instHeytingAlgebra : HeytingAlgebra Prop :=
  { Prop.instDistribLattice, Prop.instBoundedOrder with
    himp := (· → ·),
    le_himp_iff := fun _ _ _ => and_imp.symm, himp_bot := fun _ => rfl }

Heyting Algebra Structure on Propositions

Informal description

The set of propositions forms a Heyting algebra, where the Heyting implication is given by logical implication and the pseudo-complement is given by logical negation. Specifically: - The meet operation $\sqcap$ corresponds to logical conjunction (and) - The join operation $\sqcup$ corresponds to logical disjunction (or) - The implication operation $\Rightarrow$ corresponds to logical implication - The pseudo-complement $\neg$ corresponds to logical negation - The top element $\top$ corresponds to true - The bottom element $\bot$ corresponds to false This structure models intuitionistic propositional logic.

himp_iff_imp theorem

(p q : Prop) : p ⇨ q ↔ p → q

Full source

@[simp]
theorem himp_iff_imp (p q : Prop) : p ⇨ qp ⇨ q ↔ p → q :=
  Iff.rfl

Heyting Implication Equals Logical Implication in Propositional Logic

Informal description

For any propositions $p$ and $q$, the Heyting implication $p \Rightarrow q$ is equivalent to the logical implication $p \to q$.

compl_iff_not theorem

(p : Prop) : pᶜ ↔ ¬p

Full source

@[simp]
theorem compl_iff_not (p : Prop) : pᶜpᶜ ↔ ¬p :=
  Iff.rfl

Heyting Complement Equals Negation in Propositional Logic

Informal description

For any proposition $p$, the Heyting algebra complement $p^c$ is equivalent to the logical negation $\neg p$.

LinearOrder.toBiheytingAlgebra abbrev

[LinearOrder α] [BoundedOrder α] : BiheytingAlgebra α

Full source

/-- A bounded linear order is a bi-Heyting algebra by setting
* `a ⇨ b = ⊤` if `a ≤ b` and `a ⇨ b = b` otherwise.
* `a \ b = ⊥` if `a ≤ b` and `a \ b = a` otherwise. -/
abbrev LinearOrder.toBiheytingAlgebra [LinearOrder α] [BoundedOrder α] : BiheytingAlgebra α :=
  { LinearOrder.toLattice, ‹BoundedOrder α› with
    himp := fun a b => if a ≤ b then ⊤ else b,
    compl := fun a => if a = ⊥ then ⊤ else ⊥,
    le_himp_iff := fun a b c => by
      split_ifs with h
      · exact iff_of_true le_top (inf_le_of_right_le h)
      · rw [inf_le_iff, or_iff_left h],
    himp_bot := fun _ => if_congr le_bot_iff rfl rfl, sdiff := fun a b => if a ≤ b then ⊥ else a,
    hnot := fun a => if a = ⊤ then ⊥ else ⊤,
    sdiff_le_iff := fun a b c => by
      split_ifs with h
      · exact iff_of_true bot_le (le_sup_of_le_left h)
      · rw [le_sup_iff, or_iff_right h],
    top_sdiff := fun _ => if_congr top_le_iff rfl rfl }

Bi-Heyting Algebra Structure on Bounded Linear Orders

Informal description

Every bounded linear order $\alpha$ can be equipped with a bi-Heyting algebra structure, where the implication operation $\Rightarrow$ and the difference operation $\setminus$ are defined as follows: - $a \Rightarrow b = \top$ if $a \leq b$, and $a \Rightarrow b = b$ otherwise. - $a \setminus b = \bot$ if $a \leq b$, and $a \setminus b = a$ otherwise.

OrderDual.instBiheytingAlgebra instance

[BiheytingAlgebra α] : BiheytingAlgebra αᵒᵈ

Full source

instance OrderDual.instBiheytingAlgebra [BiheytingAlgebra α] : BiheytingAlgebra αᵒᵈ where
  __ := instHeytingAlgebra
  __ := instCoheytingAlgebra

Order Dual of a Bi-Heyting Algebra is a Bi-Heyting Algebra

Informal description

For any bi-Heyting algebra $\alpha$, the order dual $\alpha^{\text{op}}$ is also a bi-Heyting algebra, with the operations defined dually. Specifically: - The Heyting implication in $\alpha^{\text{op}}$ corresponds to the co-Heyting difference in $\alpha$. - The co-Heyting difference in $\alpha^{\text{op}}$ corresponds to the Heyting implication in $\alpha$. - The pseudo-complement and negation operations are swapped accordingly.

Prod.instBiheytingAlgebra instance

[BiheytingAlgebra α] [BiheytingAlgebra β] : BiheytingAlgebra (α × β)

Full source

instance Prod.instBiheytingAlgebra [BiheytingAlgebra α] [BiheytingAlgebra β] :
    BiheytingAlgebra (α × β) where
  __ := instHeytingAlgebra
  __ := instCoheytingAlgebra

Product of Bi-Heyting Algebras is a Bi-Heyting Algebra

Informal description

For any two bi-Heyting algebras $\alpha$ and $\beta$, the product $\alpha \times \beta$ is also a bi-Heyting algebra, with all operations (including implication $\Rightarrow$, difference $\setminus$, pseudo-complement $\neg$, join $\sqcup$, meet $\sqcap$, top $\top$, and bottom $\bot$) defined componentwise.

Pi.instBiheytingAlgebra instance

{α : ι → Type*} [∀ i, BiheytingAlgebra (α i)] : BiheytingAlgebra (∀ i, α i)

Full source

instance Pi.instBiheytingAlgebra {α : ι → Type*} [∀ i, BiheytingAlgebra (α i)] :
    BiheytingAlgebra (∀ i, α i) where
  __ := instHeytingAlgebra
  __ := instCoheytingAlgebra

Pointwise Bi-Heyting Algebra Structure on Product Types

Informal description

For any family of types $(\alpha_i)_{i \in \iota}$ where each $\alpha_i$ is a bi-Heyting algebra, the product type $\forall i, \alpha_i$ is also a bi-Heyting algebra, with the lattice operations, Heyting implication, co-Heyting difference, and negation operations defined pointwise.

Function.Injective.generalizedHeytingAlgebra abbrev

 [Max α] [Min α] [Top α] [HImp α] [GeneralizedHeytingAlgebra β] (f : α → β) (hf : Injective f)
  (map_sup : ∀ a b, f (a ⊔ b) = f a ⊔ f b) (map_inf : ∀ a b, f (a ⊓ b) = f a ⊓ f b) (map_top : f ⊤ = ⊤)
  (map_himp : ∀ a b, f (a ⇨ b) = f a ⇨ f b) : GeneralizedHeytingAlgebra α

Full source

/-- Pullback a `GeneralizedHeytingAlgebra` along an injection. -/
protected abbrev Function.Injective.generalizedHeytingAlgebra [Max α] [Min α] [Top α]
    [HImp α] [GeneralizedHeytingAlgebra β] (f : α → β) (hf : Injective f)
    (map_sup : ∀ a b, f (a ⊔ b) = f a ⊔ f b) (map_inf : ∀ a b, f (a ⊓ b) = f a ⊓ f b)
    (map_top : f ⊤ = ⊤) (map_himp : ∀ a b, f (a ⇨ b) = f a ⇨ f b) : GeneralizedHeytingAlgebra α :=
  { __ := hf.lattice f map_sup map_inf
    __ := ‹Top α›
    __ := ‹HImp α›
    le_top := fun a => by
      change f _ ≤ _
      rw [map_top]
      exact le_top,
    le_himp_iff := fun a b c => by
      change f _ ≤ _ ↔ f _ ≤ _
      rw [map_himp, map_inf, le_himp_iff] }

Pullback of Generalized Heyting Algebra Structure Along an Injective Function

Informal description

Let $\alpha$ and $\beta$ be types with lattice structures, where $\beta$ is a generalized Heyting algebra. Given an injective function $f \colon \alpha \to \beta$ that preserves: - Suprema: $f(a \sqcup b) = f(a) \sqcup f(b)$ for all $a, b \in \alpha$, - Infima: $f(a \sqcap b) = f(a) \sqcap f(b)$ for all $a, b \in \alpha$, - Top element: $f(\top) = \top$, - Heyting implication: $f(a \Rightarrow b) = f(a) \Rightarrow f(b)$ for all $a, b \in \alpha$, then $\alpha$ inherits a generalized Heyting algebra structure from $\beta$ via $f$.

Function.Injective.generalizedCoheytingAlgebra abbrev

 [Max α] [Min α] [Bot α] [SDiff α] [GeneralizedCoheytingAlgebra β] (f : α → β) (hf : Injective f)
  (map_sup : ∀ a b, f (a ⊔ b) = f a ⊔ f b) (map_inf : ∀ a b, f (a ⊓ b) = f a ⊓ f b) (map_bot : f ⊥ = ⊥)
  (map_sdiff : ∀ a b, f (a \ b) = f a \ f b) : GeneralizedCoheytingAlgebra α

Full source

/-- Pullback a `GeneralizedCoheytingAlgebra` along an injection. -/
protected abbrev Function.Injective.generalizedCoheytingAlgebra [Max α] [Min α] [Bot α]
    [SDiff α] [GeneralizedCoheytingAlgebra β] (f : α → β) (hf : Injective f)
    (map_sup : ∀ a b, f (a ⊔ b) = f a ⊔ f b) (map_inf : ∀ a b, f (a ⊓ b) = f a ⊓ f b)
    (map_bot : f ⊥ = ⊥) (map_sdiff : ∀ a b, f (a \ b) = f a \ f b) :
    GeneralizedCoheytingAlgebra α :=
  { __ := hf.lattice f map_sup map_inf
    __ := ‹Bot α›
    __ := ‹SDiff α›
    bot_le := fun a => by
      change f _ ≤ _
      rw [map_bot]
      exact bot_le,
    sdiff_le_iff := fun a b c => by
      change f _ ≤ _ ↔ f _ ≤ _
      rw [map_sdiff, map_sup, sdiff_le_iff] }

Pullback of Generalized Co-Heyting Algebra Structure Along an Injective Function

Informal description

Let $\alpha$ and $\beta$ be types with lattice structures, where $\beta$ is a generalized co-Heyting algebra. Given an injective function $f : \alpha \to \beta$ that preserves: - Suprema: $f(a \sqcup b) = f(a) \sqcup f(b)$ for all $a, b \in \alpha$, - Infima: $f(a \sqcap b) = f(a) \sqcap f(b)$ for all $a, b \in \alpha$, - Bottom element: $f(\bot) = \bot$, - Difference operation: $f(a \setminus b) = f(a) \setminus f(b)$ for all $a, b \in \alpha$, then $\alpha$ inherits a generalized co-Heyting algebra structure from $\beta$ via $f$.

Function.Injective.heytingAlgebra abbrev

 [Max α] [Min α] [Top α] [Bot α] [HasCompl α] [HImp α] [HeytingAlgebra β] (f : α → β) (hf : Injective f)
  (map_sup : ∀ a b, f (a ⊔ b) = f a ⊔ f b) (map_inf : ∀ a b, f (a ⊓ b) = f a ⊓ f b) (map_top : f ⊤ = ⊤)
  (map_bot : f ⊥ = ⊥) (map_compl : ∀ a, f aᶜ = (f a)ᶜ) (map_himp : ∀ a b, f (a ⇨ b) = f a ⇨ f b) : HeytingAlgebra α

Full source

/-- Pullback a `HeytingAlgebra` along an injection. -/
protected abbrev Function.Injective.heytingAlgebra [Max α] [Min α] [Top α] [Bot α]
    [HasCompl α] [HImp α] [HeytingAlgebra β] (f : α → β) (hf : Injective f)
    (map_sup : ∀ a b, f (a ⊔ b) = f a ⊔ f b) (map_inf : ∀ a b, f (a ⊓ b) = f a ⊓ f b)
    (map_top : f ⊤ = ⊤) (map_bot : f ⊥ = ⊥) (map_compl : ∀ a, f aᶜ = (f a)ᶜ)
    (map_himp : ∀ a b, f (a ⇨ b) = f a ⇨ f b) : HeytingAlgebra α :=
  { __ := hf.generalizedHeytingAlgebra f map_sup map_inf map_top map_himp
    __ := ‹Bot α›
    __ := ‹HasCompl α›
    bot_le := fun a => by
      change f _ ≤ _
      rw [map_bot]
      exact bot_le,
    himp_bot := fun a => hf <| by rw [map_himp, map_compl, map_bot, himp_bot] }

Pullback of Heyting Algebra Structure Along an Injective Function

Informal description

Let $\alpha$ and $\beta$ be types with lattice structures, where $\beta$ is a Heyting algebra. Given an injective function $f \colon \alpha \to \beta$ that preserves: - Suprema: $f(a \sqcup b) = f(a) \sqcup f(b)$ for all $a, b \in \alpha$, - Infima: $f(a \sqcap b) = f(a) \sqcap f(b)$ for all $a, b \in \alpha$, - Top element: $f(\top) = \top$, - Bottom element: $f(\bot) = \bot$, - Pseudo-complement: $f(a^c) = (f(a))^c$ for all $a \in \alpha$, - Heyting implication: $f(a \Rightarrow b) = f(a) \Rightarrow f(b)$ for all $a, b \in \alpha$, then $\alpha$ inherits a Heyting algebra structure from $\beta$ via $f$.

Function.Injective.coheytingAlgebra abbrev

 [Max α] [Min α] [Top α] [Bot α] [HNot α] [SDiff α] [CoheytingAlgebra β] (f : α → β) (hf : Injective f)
  (map_sup : ∀ a b, f (a ⊔ b) = f a ⊔ f b) (map_inf : ∀ a b, f (a ⊓ b) = f a ⊓ f b) (map_top : f ⊤ = ⊤)
  (map_bot : f ⊥ = ⊥) (map_hnot : ∀ a, f (￢a) = ￢f a) (map_sdiff : ∀ a b, f (a \ b) = f a \ f b) : CoheytingAlgebra α

Full source

/-- Pullback a `CoheytingAlgebra` along an injection. -/
protected abbrev Function.Injective.coheytingAlgebra [Max α] [Min α] [Top α] [Bot α]
    [HNot α] [SDiff α] [CoheytingAlgebra β] (f : α → β) (hf : Injective f)
    (map_sup : ∀ a b, f (a ⊔ b) = f a ⊔ f b) (map_inf : ∀ a b, f (a ⊓ b) = f a ⊓ f b)
    (map_top : f ⊤ = ⊤) (map_bot : f ⊥ = ⊥) (map_hnot : ∀ a, f (￢a) = ￢f a)
    (map_sdiff : ∀ a b, f (a \ b) = f a \ f b) : CoheytingAlgebra α :=
  { __ := hf.generalizedCoheytingAlgebra f map_sup map_inf map_bot map_sdiff
    __ := ‹Top α›
    __ := ‹HNot α›
    le_top := fun a => by
      change f _ ≤ _
      rw [map_top]
      exact le_top,
    top_sdiff := fun a => hf <| by rw [map_sdiff, map_hnot, map_top, top_sdiff'] }

Pullback of Co-Heyting Algebra Structure Along an Injective Function

Informal description

Let $\alpha$ and $\beta$ be types with lattice structures, where $\beta$ is a co-Heyting algebra. Given an injective function $f : \alpha \to \beta$ that preserves: - Suprema: $f(a \sqcup b) = f(a) \sqcup f(b)$ for all $a, b \in \alpha$, - Infima: $f(a \sqcap b) = f(a) \sqcap f(b)$ for all $a, b \in \alpha$, - Top element: $f(\top) = \top$, - Bottom element: $f(\bot) = \bot$, - Negation: $f(\neg a) = \neg f(a)$ for all $a \in \alpha$, - Difference operation: $f(a \setminus b) = f(a) \setminus f(b)$ for all $a, b \in \alpha$, then $\alpha$ inherits a co-Heyting algebra structure from $\beta$ via $f$.

Function.Injective.biheytingAlgebra abbrev

 [Max α] [Min α] [Top α] [Bot α] [HasCompl α] [HNot α] [HImp α] [SDiff α] [BiheytingAlgebra β] (f : α → β)
  (hf : Injective f) (map_sup : ∀ a b, f (a ⊔ b) = f a ⊔ f b) (map_inf : ∀ a b, f (a ⊓ b) = f a ⊓ f b)
  (map_top : f ⊤ = ⊤) (map_bot : f ⊥ = ⊥) (map_compl : ∀ a, f aᶜ = (f a)ᶜ) (map_hnot : ∀ a, f (￢a) = ￢f a)
  (map_himp : ∀ a b, f (a ⇨ b) = f a ⇨ f b) (map_sdiff : ∀ a b, f (a \ b) = f a \ f b) : BiheytingAlgebra α

Full source

/-- Pullback a `BiheytingAlgebra` along an injection. -/
protected abbrev Function.Injective.biheytingAlgebra [Max α] [Min α] [Top α] [Bot α]
    [HasCompl α] [HNot α] [HImp α] [SDiff α] [BiheytingAlgebra β] (f : α → β)
    (hf : Injective f) (map_sup : ∀ a b, f (a ⊔ b) = f a ⊔ f b)
    (map_inf : ∀ a b, f (a ⊓ b) = f a ⊓ f b) (map_top : f ⊤ = ⊤) (map_bot : f ⊥ = ⊥)
    (map_compl : ∀ a, f aᶜ = (f a)ᶜ) (map_hnot : ∀ a, f (￢a) = ￢f a)
    (map_himp : ∀ a b, f (a ⇨ b) = f a ⇨ f b) (map_sdiff : ∀ a b, f (a \ b) = f a \ f b) :
    BiheytingAlgebra α :=
  { hf.heytingAlgebra f map_sup map_inf map_top map_bot map_compl map_himp,
    hf.coheytingAlgebra f map_sup map_inf map_top map_bot map_hnot map_sdiff with }

Pullback of Bi-Heyting Algebra Structure Along an Injective Function

Informal description

Let $\alpha$ and $\beta$ be types with lattice structures, where $\beta$ is a bi-Heyting algebra. Given an injective function $f \colon \alpha \to \beta$ that preserves: - Suprema: $f(a \sqcup b) = f(a) \sqcup f(b)$ for all $a, b \in \alpha$, - Infima: $f(a \sqcap b) = f(a) \sqcap f(b)$ for all $a, b \in \alpha$, - Top element: $f(\top) = \top$, - Bottom element: $f(\bot) = \bot$, - Pseudo-complement: $f(a^c) = (f(a))^c$ for all $a \in \alpha$, - Negation: $f(\neg a) = \neg f(a)$ for all $a \in \alpha$, - Heyting implication: $f(a \Rightarrow b) = f(a) \Rightarrow f(b)$ for all $a, b \in \alpha$, - Difference operation: $f(a \setminus b) = f(a) \setminus f(b)$ for all $a, b \in \alpha$, then $\alpha$ inherits a bi-Heyting algebra structure from $\beta$ via $f$.

PUnit.instBiheytingAlgebra instance

: BiheytingAlgebra PUnit.{u + 1}

Full source

instance instBiheytingAlgebra : BiheytingAlgebra PUnitPUnit.{u+1} :=
  { PUnit.instLinearOrderPUnit.instLinearOrder.{u} with
    top := unit,
    bot := unit,
    sup := fun _ _ => unit,
    inf := fun _ _ => unit,
    compl := fun _ => unit,
    sdiff := fun _ _ => unit,
    hnot := fun _ => unit,
    himp := fun _ _ => unit,
    le_top := fun _ => trivial,
    le_sup_left := fun _ _ => trivial,
    le_sup_right := fun _ _ => trivial,
    sup_le := fun _ _ _ _ _ => trivial,
    inf_le_left := fun _ _ => trivial,
    inf_le_right := fun _ _ => trivial,
    le_inf := fun _ _ _ _ _ => trivial,
    bot_le := fun _ => trivial,
    le_himp_iff := fun _ _ _ => Iff.rfl,
    himp_bot := fun _ => rfl,
    top_sdiff := fun _ => rfl,
    sdiff_le_iff := fun _ _ _ => Iff.rfl }

Bi-Heyting Algebra Structure on the Trivial Type

Informal description

The trivial type `PUnit` (the type with a single element) has a canonical bi-Heyting algebra structure, where all operations (implication `⇨`, difference `\`, pseudo-complement `ᶜ`, and negation `￢`) are defined in the trivial way.

PUnit.top_eq theorem

: (⊤ : PUnit) = unit

Full source

@[simp]
theorem top_eq : (⊤ : PUnit) = unit :=
  rfl

Top Element in Trivial Type Equals Unique Element

Informal description

In the trivial type `PUnit` (the type with a single element), the top element `⊤` is equal to the unique element `unit`.

PUnit.bot_eq theorem

: (⊥ : PUnit) = unit

Full source

@[simp]
theorem bot_eq : (⊥ : PUnit) = unit :=
  rfl

Bottom Element in Trivial Type Equals Unit

Informal description

In the trivial type `PUnit` (the type with a single element), the bottom element `⊥` is equal to the unique element `unit`.

PUnit.sup_eq theorem

: a ⊔ b = unit

Full source

@[simp]
theorem sup_eq : a ⊔ b = unit :=
  rfl

Join Operation in Trivial Type Equals Unit

Informal description

For any elements $a$ and $b$ in the trivial type `PUnit`, the join (supremum) $a \sqcup b$ is equal to the unique element `unit` of `PUnit`.

PUnit.inf_eq theorem

: a ⊓ b = unit

Full source

@[simp]
theorem inf_eq : a ⊓ b = unit :=
  rfl

Meet in Trivial Type is Unit

Informal description

For any elements $a$ and $b$ in the trivial type `PUnit`, their meet (infimum) $a \sqcap b$ is equal to the unique element `unit` of `PUnit`.

PUnit.compl_eq theorem

: aᶜ = unit

Full source

@[simp]
theorem compl_eq : aᶜ = unit :=
  rfl

Pseudo-complement in Trivial Bi-Heyting Algebra

Informal description

In the trivial bi-Heyting algebra structure on the singleton type `PUnit`, the pseudo-complement of any element is the unique element of the type, i.e., $a^c = \text{unit}$ for all $a \in \text{PUnit}$.

PUnit.sdiff_eq theorem

: a \ b = unit

Full source

@[simp]
theorem sdiff_eq : a \ b = unit :=
  rfl

Difference Operation in Trivial Bi-Heyting Algebra

Informal description

In the bi-Heyting algebra structure on the trivial type `PUnit`, the difference operation `\` between any two elements `a` and `b` is equal to the unique element `unit` of `PUnit`.

PUnit.hnot_eq theorem

: ￢a = unit

Full source

@[simp]
theorem hnot_eq : ￢a = unit :=
  rfl

Negation in Trivial Bi-Heyting Algebra is Constant

Informal description

In the trivial bi-Heyting algebra structure on the singleton type `PUnit`, the negation operation satisfies $￢a = \text{unit}$ for any element $a$.

PUnit.himp_eq theorem

: a ⇨ b = unit

Full source

@[simp]
theorem himp_eq : a ⇨ b = unit :=
  rfl

Implication in Trivial Heyting Algebra is Constant

Informal description

In the trivial Heyting algebra structure on the singleton type `PUnit`, the implication operation `⇨` satisfies $a \ ⇨ \ b = \text{unit}$ for any elements $a, b$ of `PUnit`.

Mathlib.Order.Heyting.Basic

Main declarations

References

Tags