Heyting algebras

This file defines Heyting, co-Heyting and bi-Heyting algebras.

A Heyting algebra is a bounded distributive lattice with an implication operation ⇨ such that a ≤ b ⇨ c ↔ a ⊓ b ≤ c. It also comes with a pseudo-complement ᶜ, such that aᶜ = a ⇨ ⊥.

Co-Heyting algebras are dual to Heyting algebras. They have a difference \ and a negation ￢ such that a \ b ≤ c ↔ a ≤ b ⊔ c and ￢a = ⊤ \ a.

Bi-Heyting algebras are Heyting algebras that are also co-Heyting algebras.

From a logic standpoint, Heyting algebras precisely model intuitionistic logic, whereas boolean algebras model classical logic.

Heyting algebras are the order theoretic equivalent of cartesian-closed categories.

Main declarations

• GeneralizedHeytingAlgebra: Heyting algebra without a top element (nor negation).
• GeneralizedCoheytingAlgebra: Co-Heyting algebra without a bottom element (nor complement).
• HeytingAlgebra: Heyting algebra.
• CoheytingAlgebra: Co-Heyting algebra.
• BiheytingAlgebra: bi-Heyting algebra.

References

• [Francis Borceux, Handbook of Categorical Algebra III][borceux-vol3]

Tags

Heyting, Brouwer, algebra, implication, negation, intuitionistic

Notation

instance Prod.instHImp (α : Type u_2) (β : Type u_3) [HImp α] [HImp β] : HImp (α × β)

Equations

• Prod.instHImp α β = { himp := fun (a b : α × β) => (a.1 ⇨ b.1, a.2 ⇨ b.2) }

instance Prod.instHNot (α : Type u_2) (β : Type u_3) [HNot α] [HNot β] : HNot (α × β)

Equations

• Prod.instHNot α β = { hnot := fun (a : α × β) => (￢a.1, ￢a.2) }

instance Prod.instSDiff (α : Type u_2) (β : Type u_3) [SDiff α] [SDiff β] : SDiff (α × β)

Equations

• Prod.instSDiff α β = { sdiff := fun (a b : α × β) => (a.1 \ b.1, a.2 \ b.2) }

instance Prod.instHasCompl (α : Type u_2) (β : Type u_3) [HasCompl α] [HasCompl β] : HasCompl (α × β)

Equations

• Prod.instHasCompl α β = { compl := fun (a : α × β) => (a.1ᶜ, a.2ᶜ) }

@[simp]

theorem fst_himp {α : Type u_2} {β : Type u_3} [HImp α] [HImp β] (a : α × β) (b : α × β) : (a ⇨ b).1 = a.1 ⇨ b.1

@[simp]

theorem snd_himp {α : Type u_2} {β : Type u_3} [HImp α] [HImp β] (a : α × β) (b : α × β) : (a ⇨ b).2 = a.2 ⇨ b.2

@[simp]

theorem fst_hnot {α : Type u_2} {β : Type u_3} [HNot α] [HNot β] (a : α × β) : (￢a).1 = ￢a.1

@[simp]

theorem snd_hnot {α : Type u_2} {β : Type u_3} [HNot α] [HNot β] (a : α × β) : (￢a).2 = ￢a.2

@[simp]

theorem fst_sdiff {α : Type u_2} {β : Type u_3} [SDiff α] [SDiff β] (a : α × β) (b : α × β) : (a \ b).1 = a.1 \ b.1

@[simp]

theorem snd_sdiff {α : Type u_2} {β : Type u_3} [SDiff α] [SDiff β] (a : α × β) (b : α × β) : (a \ b).2 = a.2 \ b.2

@[simp]

theorem fst_compl {α : Type u_2} {β : Type u_3} [HasCompl α] [HasCompl β] (a : α × β) : aᶜ.1 = a.1ᶜ

@[simp]

theorem snd_compl {α : Type u_2} {β : Type u_3} [HasCompl α] [HasCompl β] (a : α × β) : aᶜ.2 = a.2ᶜ

instance Pi.instHImpForall {ι : Type u_1} {π : ι → Type u_4} [(i : ι) → HImp (π i)] : HImp ((i : ι) → π i)

Equations

• Pi.instHImpForall = { himp := fun (a b : (i : ι) → π i) (i : ι) => a i ⇨ b i }

instance Pi.instHNotForall {ι : Type u_1} {π : ι → Type u_4} [(i : ι) → HNot (π i)] : HNot ((i : ι) → π i)

Equations

• Pi.instHNotForall = { hnot := fun (a : (i : ι) → π i) (i : ι) => ￢a i }

theorem Pi.himp_def {ι : Type u_1} {π : ι → Type u_4} [(i : ι) → HImp (π i)] (a : (i : ι) → π i) (b : (i : ι) → π i) : a ⇨ b = fun (i : ι) => a i ⇨ b i

theorem Pi.hnot_def {ι : Type u_1} {π : ι → Type u_4} [(i : ι) → HNot (π i)] (a : (i : ι) → π i) : ￢a = fun (i : ι) => ￢a i

@[simp]

theorem Pi.himp_apply {ι : Type u_1} {π : ι → Type u_4} [(i : ι) → HImp (π i)] (a : (i : ι) → π i) (b : (i : ι) → π i) (i : ι) : (a ⇨ b) i = a i ⇨ b i

@[simp]

theorem Pi.hnot_apply {ι : Type u_1} {π : ι → Type u_4} [(i : ι) → HNot (π i)] (a : (i : ι) → π i) (i : ι) : (￢a) i = ￢a i

class GeneralizedHeytingAlgebra (α : Type u_4) extends Lattice , OrderTop , HImp : Type u_4

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.

• sup : α → α → α
• le : α → α → Prop
• lt : α → α → Prop
• le_refl : ∀ (a : α), a ≤ a
• le_trans : ∀ (a b c : α), a ≤ b → b ≤ c → a ≤ c
• lt_iff_le_not_le : ∀ (a b : α), a < b ↔ a ≤ b ∧ ¬b ≤ a
• le_antisymm : ∀ (a b : α), a ≤ b → b ≤ a → a = b
• le_sup_left : ∀ (a b : α), a ≤ a ⊔ b
• le_sup_right : ∀ (a b : α), b ≤ a ⊔ b
• sup_le : ∀ (a b c : α), a ≤ c → b ≤ c → a ⊔ b ≤ c
• inf : α → α → α
• inf_le_left : ∀ (a b : α), a ⊓ b ≤ a
• inf_le_right : ∀ (a b : α), a ⊓ b ≤ b
• le_inf : ∀ (a b c : α), a ≤ b → a ≤ c → a ≤ b ⊓ c
• top : α
• le_top : ∀ (a : α), a ≤ ⊤
• himp : α → α → α
• le_himp_iff : ∀ (a b c : α), a ≤ b ⇨ c ↔ a ⊓ b ≤ c

  (a ⇨ ·) is right adjoint to (a ⊓ ·)

theorem GeneralizedHeytingAlgebra.le_himp_iff {α : Type u_4} [self : GeneralizedHeytingAlgebra α] (a : α) (b : α) (c : α) : a ≤ b ⇨ c ↔ a ⊓ b ≤ c

(a ⇨ ·) is right adjoint to (a ⊓ ·)

class GeneralizedCoheytingAlgebra (α : Type u_4) extends Lattice , OrderBot , SDiff : Type u_4

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

This generalizes CoheytingAlgebra by not requiring a top element.

• sup : α → α → α
• le : α → α → Prop
• lt : α → α → Prop
• le_refl : ∀ (a : α), a ≤ a
• le_trans : ∀ (a b c : α), a ≤ b → b ≤ c → a ≤ c
• lt_iff_le_not_le : ∀ (a b : α), a < b ↔ a ≤ b ∧ ¬b ≤ a
• le_antisymm : ∀ (a b : α), a ≤ b → b ≤ a → a = b
• le_sup_left : ∀ (a b : α), a ≤ a ⊔ b
• le_sup_right : ∀ (a b : α), b ≤ a ⊔ b
• sup_le : ∀ (a b c : α), a ≤ c → b ≤ c → a ⊔ b ≤ c
• inf : α → α → α
• inf_le_left : ∀ (a b : α), a ⊓ b ≤ a
• inf_le_right : ∀ (a b : α), a ⊓ b ≤ b
• le_inf : ∀ (a b c : α), a ≤ b → a ≤ c → a ≤ b ⊓ c
• bot : α
• bot_le : ∀ (a : α), ⊥ ≤ a
• sdiff : α → α → α
• sdiff_le_iff : ∀ (a b c : α), a \ b ≤ c ↔ a ≤ b ⊔ c

  (· \ a) is right adjoint to (· ⊔ a)

theorem GeneralizedCoheytingAlgebra.sdiff_le_iff {α : Type u_4} [self : GeneralizedCoheytingAlgebra α] (a : α) (b : α) (c : α) : a \ b ≤ c ↔ a ≤ b ⊔ c

(· \ a) is right adjoint to (· ⊔ a)

class HeytingAlgebra (α : Type u_4) extends GeneralizedHeytingAlgebra , OrderBot , HasCompl : Type u_4

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

• sup : α → α → α
• le : α → α → Prop
• lt : α → α → Prop
• le_refl : ∀ (a : α), a ≤ a
• le_trans : ∀ (a b c : α), a ≤ b → b ≤ c → a ≤ c
• lt_iff_le_not_le : ∀ (a b : α), a < b ↔ a ≤ b ∧ ¬b ≤ a
• le_antisymm : ∀ (a b : α), a ≤ b → b ≤ a → a = b
• le_sup_left : ∀ (a b : α), a ≤ a ⊔ b
• le_sup_right : ∀ (a b : α), b ≤ a ⊔ b
• sup_le : ∀ (a b c : α), a ≤ c → b ≤ c → a ⊔ b ≤ c
• inf : α → α → α
• inf_le_left : ∀ (a b : α), a ⊓ b ≤ a
• inf_le_right : ∀ (a b : α), a ⊓ b ≤ b
• le_inf : ∀ (a b c : α), a ≤ b → a ≤ c → a ≤ b ⊓ c
• top : α
• le_top : ∀ (a : α), a ≤ ⊤
• himp : α → α → α
• le_himp_iff : ∀ (a b c : α), a ≤ b ⇨ c ↔ a ⊓ b ≤ c
• bot : α
• bot_le : ∀ (a : α), ⊥ ≤ a
• compl : α → α
• himp_bot : ∀ (a : α), a ⇨ ⊥ = aᶜ

  aᶜ is defined as a ⇨ ⊥

theorem HeytingAlgebra.himp_bot {α : Type u_4} [self : HeytingAlgebra α] (a : α) : a ⇨ ⊥ = aᶜ

aᶜ is defined as a ⇨ ⊥

class CoheytingAlgebra (α : Type u_4) extends GeneralizedCoheytingAlgebra , OrderTop , HNot : Type u_4

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

• sup : α → α → α
• le : α → α → Prop
• lt : α → α → Prop
• le_refl : ∀ (a : α), a ≤ a
• le_trans : ∀ (a b c : α), a ≤ b → b ≤ c → a ≤ c
• lt_iff_le_not_le : ∀ (a b : α), a < b ↔ a ≤ b ∧ ¬b ≤ a
• le_antisymm : ∀ (a b : α), a ≤ b → b ≤ a → a = b
• le_sup_left : ∀ (a b : α), a ≤ a ⊔ b
• le_sup_right : ∀ (a b : α), b ≤ a ⊔ b
• sup_le : ∀ (a b c : α), a ≤ c → b ≤ c → a ⊔ b ≤ c
• inf : α → α → α
• inf_le_left : ∀ (a b : α), a ⊓ b ≤ a
• inf_le_right : ∀ (a b : α), a ⊓ b ≤ b
• le_inf : ∀ (a b c : α), a ≤ b → a ≤ c → a ≤ b ⊓ c
• bot : α
• bot_le : ∀ (a : α), ⊥ ≤ a
• sdiff : α → α → α
• sdiff_le_iff : ∀ (a b c : α), a \ b ≤ c ↔ a ≤ b ⊔ c
• top : α
• le_top : ∀ (a : α), a ≤ ⊤
• hnot : α → α
• top_sdiff : ∀ (a : α), ⊤ \ a = ￢a

  ⊤ \ a is ￢a

theorem CoheytingAlgebra.top_sdiff {α : Type u_4} [self : CoheytingAlgebra α] (a : α) : ⊤ \ a = ￢a

⊤ \ a is ￢a

class BiheytingAlgebra (α : Type u_4) extends HeytingAlgebra , SDiff , HNot : Type u_4

A bi-Heyting algebra is a Heyting algebra that is also a co-Heyting algebra.

• sup : α → α → α
• le : α → α → Prop
• lt : α → α → Prop
• le_refl : ∀ (a : α), a ≤ a
• le_trans : ∀ (a b c : α), a ≤ b → b ≤ c → a ≤ c
• lt_iff_le_not_le : ∀ (a b : α), a < b ↔ a ≤ b ∧ ¬b ≤ a
• le_antisymm : ∀ (a b : α), a ≤ b → b ≤ a → a = b
• le_sup_left : ∀ (a b : α), a ≤ a ⊔ b
• le_sup_right : ∀ (a b : α), b ≤ a ⊔ b
• sup_le : ∀ (a b c : α), a ≤ c → b ≤ c → a ⊔ b ≤ c
• inf : α → α → α
• inf_le_left : ∀ (a b : α), a ⊓ b ≤ a
• inf_le_right : ∀ (a b : α), a ⊓ b ≤ b
• le_inf : ∀ (a b c : α), a ≤ b → a ≤ c → a ≤ b ⊓ c
• top : α
• le_top : ∀ (a : α), a ≤ ⊤
• himp : α → α → α
• le_himp_iff : ∀ (a b c : α), a ≤ b ⇨ c ↔ a ⊓ b ≤ c
• bot : α
• bot_le : ∀ (a : α), ⊥ ≤ a
• compl : α → α
• himp_bot : ∀ (a : α), a ⇨ ⊥ = aᶜ
• sdiff : α → α → α
• hnot : α → α
• sdiff_le_iff : ∀ (a b c : α), a \ b ≤ c ↔ a ≤ b ⊔ c

  (· \ a) is right adjoint to (· ⊔ a)

• top_sdiff : ∀ (a : α), ⊤ \ a = ￢a

  ⊤ \ a is ￢a

theorem BiheytingAlgebra.sdiff_le_iff {α : Type u_4} [self : BiheytingAlgebra α] (a : α) (b : α) (c : α) : a \ b ≤ c ↔ a ≤ b ⊔ c

(· \ a) is right adjoint to (· ⊔ a)

theorem BiheytingAlgebra.top_sdiff {α : Type u_4} [self : BiheytingAlgebra α] (a : α) : ⊤ \ a = ￢a

⊤ \ a is ￢a

@[instance 100]

instance HeytingAlgebra.toBoundedOrder {α : Type u_2} [HeytingAlgebra α] : BoundedOrder α

Equations

• HeytingAlgebra.toBoundedOrder = BoundedOrder.mk

@[instance 100]

instance CoheytingAlgebra.toBoundedOrder {α : Type u_2} [CoheytingAlgebra α] : BoundedOrder α

Equations

• CoheytingAlgebra.toBoundedOrder = BoundedOrder.mk

@[instance 100]

instance BiheytingAlgebra.toCoheytingAlgebra {α : Type u_2} [BiheytingAlgebra α] : CoheytingAlgebra α

Equations

• BiheytingAlgebra.toCoheytingAlgebra = CoheytingAlgebra.mk ⋯

@[reducible, inline]

abbrev HeytingAlgebra.ofHImp {α : Type u_2} [DistribLattice α] [BoundedOrder α] (himp : α → α → α) (le_himp_iff : ∀ (a b c : α), a ≤ himp b c ↔ a ⊓ b ≤ c) : HeytingAlgebra α

Construct a Heyting algebra from the lattice structure and Heyting implication alone.

Equations

• HeytingAlgebra.ofHImp himp le_himp_iff = HeytingAlgebra.mk ⋯

@[reducible, inline]

abbrev HeytingAlgebra.ofCompl {α : Type u_2} [DistribLattice α] [BoundedOrder α] (compl : α → α) (le_himp_iff : ∀ (a b c : α), a ≤ compl b ⊔ c ↔ a ⊓ b ≤ c) : HeytingAlgebra α

Construct a Heyting algebra from the lattice structure and complement operator alone.

Equations

• HeytingAlgebra.ofCompl compl le_himp_iff = HeytingAlgebra.mk ⋯

@[reducible, inline]

abbrev CoheytingAlgebra.ofSDiff {α : Type u_2} [DistribLattice α] [BoundedOrder α] (sdiff : α → α → α) (sdiff_le_iff : ∀ (a b c : α), sdiff a b ≤ c ↔ a ≤ b ⊔ c) : CoheytingAlgebra α

Construct a co-Heyting algebra from the lattice structure and the difference alone.

Equations

• CoheytingAlgebra.ofSDiff sdiff sdiff_le_iff = CoheytingAlgebra.mk ⋯

@[reducible, inline]

abbrev CoheytingAlgebra.ofHNot {α : Type u_2} [DistribLattice α] [BoundedOrder α] (hnot : α → α) (sdiff_le_iff : ∀ (a b c : α), a ⊓ hnot b ≤ c ↔ a ≤ b ⊔ c) : CoheytingAlgebra α

Construct a co-Heyting algebra from the difference and Heyting negation alone.

Equations

• CoheytingAlgebra.ofHNot hnot sdiff_le_iff = CoheytingAlgebra.mk ⋯

In this section, we'll give interpretations of these results in the Heyting algebra model of intuitionistic logic,- where ≤ can be interpreted as "validates", ⇨ as "implies", ⊓ as "and", ⊔ as "or", ⊥ as "false" and ⊤ as "true". Note that we confuse → and ⊢ because those are the same in this logic.

See also Prop.heytingAlgebra.

@[simp]

theorem le_himp_iff {α : Type u_2} [GeneralizedHeytingAlgebra α] {a : α} {b : α} {c : α} : a ≤ b ⇨ c ↔ a ⊓ b ≤ c

p → q → r ↔ p ∧ q → r

theorem le_himp_iff' {α : Type u_2} [GeneralizedHeytingAlgebra α] {a : α} {b : α} {c : α} : a ≤ b ⇨ c ↔ b ⊓ a ≤ c

p → q → r ↔ q ∧ p → r

theorem le_himp_comm {α : Type u_2} [GeneralizedHeytingAlgebra α] {a : α} {b : α} {c : α} : a ≤ b ⇨ c ↔ b ≤ a ⇨ c

p → q → r ↔ q → p → r

theorem le_himp {α : Type u_2} [GeneralizedHeytingAlgebra α] {a : α} {b : α} : a ≤ b ⇨ a

p → q → p

theorem le_himp_iff_left {α : Type u_2} [GeneralizedHeytingAlgebra α] {a : α} {b : α} : a ≤ a ⇨ b ↔ a ≤ b

p → p → q ↔ p → q

@[simp]

theorem himp_self {α : Type u_2} [GeneralizedHeytingAlgebra α] {a : α} : a ⇨ a = ⊤

p → p

theorem himp_inf_le {α : Type u_2} [GeneralizedHeytingAlgebra α] {a : α} {b : α} : (a ⇨ b) ⊓ a ≤ b

(p → q) ∧ p → q

theorem inf_himp_le {α : Type u_2} [GeneralizedHeytingAlgebra α] {a : α} {b : α} : a ⊓ (a ⇨ b) ≤ b

p ∧ (p → q) → q

@[simp]

theorem inf_himp {α : Type u_2} [GeneralizedHeytingAlgebra α] (a : α) (b : α) : a ⊓ (a ⇨ b) = a ⊓ b

p ∧ (p → q) ↔ p ∧ q

@[simp]

theorem himp_inf_self {α : Type u_2} [GeneralizedHeytingAlgebra α] (a : α) (b : α) : (a ⇨ b) ⊓ a = b ⊓ a

(p → q) ∧ p ↔ q ∧ p

@[simp]

theorem himp_eq_top_iff {α : Type u_2} [GeneralizedHeytingAlgebra α] {a : α} {b : α} : a ⇨ b = ⊤ ↔ a ≤ b

The deduction theorem in the Heyting algebra model of intuitionistic logic: an implication holds iff the conclusion follows from the hypothesis.

@[simp]

theorem himp_top {α : Type u_2} [GeneralizedHeytingAlgebra α] {a : α} : a ⇨ ⊤ = ⊤

p → true, true → p ↔ p

@[simp]

theorem top_himp {α : Type u_2} [GeneralizedHeytingAlgebra α] {a : α} : ⊤ ⇨ a = a

theorem himp_himp {α : Type u_2} [GeneralizedHeytingAlgebra α] (a : α) (b : α) (c : α) : a ⇨ b ⇨ c = a ⊓ b ⇨ c

p → q → r ↔ p ∧ q → r

theorem himp_le_himp_himp_himp {α : Type u_2} [GeneralizedHeytingAlgebra α] {a : α} {b : α} {c : α} : b ⇨ c ≤ (a ⇨ b) ⇨ a ⇨ c

(q → r) → (p → q) → q → r

@[simp]

theorem himp_inf_himp_inf_le {α : Type u_2} [GeneralizedHeytingAlgebra α] {a : α} {b : α} {c : α} : (b ⇨ c) ⊓ (a ⇨ b) ⊓ a ≤ c

theorem himp_left_comm {α : Type u_2} [GeneralizedHeytingAlgebra α] (a : α) (b : α) (c : α) : a ⇨ b ⇨ c = b ⇨ a ⇨ c

p → q → r ↔ q → p → r

@[simp]

theorem himp_idem {α : Type u_2} [GeneralizedHeytingAlgebra α] {a : α} {b : α} : b ⇨ b ⇨ a = b ⇨ a

theorem himp_inf_distrib {α : Type u_2} [GeneralizedHeytingAlgebra α] (a : α) (b : α) (c : α) : a ⇨ b ⊓ c = (a ⇨ b) ⊓ (a ⇨ c)

theorem sup_himp_distrib {α : Type u_2} [GeneralizedHeytingAlgebra α] (a : α) (b : α) (c : α) : a ⊔ b ⇨ c = (a ⇨ c) ⊓ (b ⇨ c)

theorem himp_le_himp_left {α : Type u_2} [GeneralizedHeytingAlgebra α] {a : α} {b : α} {c : α} (h : a ≤ b) : c ⇨ a ≤ c ⇨ b

theorem himp_le_himp_right {α : Type u_2} [GeneralizedHeytingAlgebra α] {a : α} {b : α} {c : α} (h : a ≤ b) : b ⇨ c ≤ a ⇨ c

theorem himp_le_himp {α : Type u_2} [GeneralizedHeytingAlgebra α] {a : α} {b : α} {c : α} {d : α} (hab : a ≤ b) (hcd : c ≤ d) : b ⇨ c ≤ a ⇨ d

@[simp]

theorem sup_himp_self_left {α : Type u_2} [GeneralizedHeytingAlgebra α] (a : α) (b : α) : a ⊔ b ⇨ a = b ⇨ a

@[simp]

theorem sup_himp_self_right {α : Type u_2} [GeneralizedHeytingAlgebra α] (a : α) (b : α) : a ⊔ b ⇨ b = a ⇨ b

theorem Codisjoint.himp_eq_right {α : Type u_2} [GeneralizedHeytingAlgebra α] {a : α} {b : α} (h : Codisjoint a b) : b ⇨ a = a

theorem Codisjoint.himp_eq_left {α : Type u_2} [GeneralizedHeytingAlgebra α] {a : α} {b : α} (h : Codisjoint a b) : a ⇨ b = b

theorem Codisjoint.himp_inf_cancel_right {α : Type u_2} [GeneralizedHeytingAlgebra α] {a : α} {b : α} (h : Codisjoint a b) : a ⇨ a ⊓ b = b

theorem Codisjoint.himp_inf_cancel_left {α : Type u_2} [GeneralizedHeytingAlgebra α] {a : α} {b : α} (h : Codisjoint a b) : b ⇨ a ⊓ b = a

theorem Codisjoint.himp_le_of_right_le {α : Type u_2} [GeneralizedHeytingAlgebra α] {a : α} {b : α} {c : α} (hac : Codisjoint a c) (hba : b ≤ a) : c ⇨ b ≤ a

See himp_le for a stronger version in Boolean algebras.

theorem le_himp_himp {α : Type u_2} [GeneralizedHeytingAlgebra α] {a : α} {b : α} : a ≤ (a ⇨ b) ⇨ b

@[simp]

theorem himp_eq_himp_iff {α : Type u_2} [GeneralizedHeytingAlgebra α] {a : α} {b : α} : b ⇨ a = a ⇨ b ↔ a = b

theorem himp_ne_himp_iff {α : Type u_2} [GeneralizedHeytingAlgebra α] {a : α} {b : α} : b ⇨ a ≠ a ⇨ b ↔ a ≠ b

theorem himp_triangle {α : Type u_2} [GeneralizedHeytingAlgebra α] (a : α) (b : α) (c : α) : (a ⇨ b) ⊓ (b ⇨ c) ≤ a ⇨ c

theorem himp_inf_himp_cancel {α : Type u_2} [GeneralizedHeytingAlgebra α] {a : α} {b : α} {c : α} (hba : b ≤ a) (hcb : c ≤ b) : (a ⇨ b) ⊓ (b ⇨ c) = a ⇨ c

@[instance 100]

instance GeneralizedHeytingAlgebra.toDistribLattice {α : Type u_2} [GeneralizedHeytingAlgebra α] : DistribLattice α

Equations

• GeneralizedHeytingAlgebra.toDistribLattice = DistribLattice.ofInfSupLe ⋯

instance OrderDual.instGeneralizedCoheytingAlgebra {α : Type u_2} [GeneralizedHeytingAlgebra α] : GeneralizedCoheytingAlgebra αᵒᵈ

Equations

• OrderDual.instGeneralizedCoheytingAlgebra = GeneralizedCoheytingAlgebra.mk ⋯

instance Prod.instGeneralizedHeytingAlgebra {α : Type u_2} {β : Type u_3} [GeneralizedHeytingAlgebra α] [GeneralizedHeytingAlgebra β] : GeneralizedHeytingAlgebra (α × β)

Equations

• Prod.instGeneralizedHeytingAlgebra = GeneralizedHeytingAlgebra.mk ⋯

instance Pi.instGeneralizedHeytingAlgebra {ι : Type u_1} {α : ι → Type u_4} [(i : ι) → GeneralizedHeytingAlgebra (α i)] : GeneralizedHeytingAlgebra ((i : ι) → α i)

Equations

• Pi.instGeneralizedHeytingAlgebra = GeneralizedHeytingAlgebra.mk ⋯

@[simp]

theorem sdiff_le_iff {α : Type u_2} [GeneralizedCoheytingAlgebra α] {a : α} {b : α} {c : α} : a \ b ≤ c ↔ a ≤ b ⊔ c

theorem sdiff_le_iff' {α : Type u_2} [GeneralizedCoheytingAlgebra α] {a : α} {b : α} {c : α} : a \ b ≤ c ↔ a ≤ c ⊔ b

theorem sdiff_le_comm {α : Type u_2} [GeneralizedCoheytingAlgebra α] {a : α} {b : α} {c : α} : a \ b ≤ c ↔ a \ c ≤ b

theorem sdiff_le {α : Type u_2} [GeneralizedCoheytingAlgebra α] {a : α} {b : α} : a \ b ≤ a

theorem Disjoint.disjoint_sdiff_left {α : Type u_2} [GeneralizedCoheytingAlgebra α] {a : α} {b : α} {c : α} (h : Disjoint a b) : Disjoint (a \ c) b

theorem Disjoint.disjoint_sdiff_right {α : Type u_2} [GeneralizedCoheytingAlgebra α] {a : α} {b : α} {c : α} (h : Disjoint a b) : Disjoint a (b \ c)

theorem sdiff_le_iff_left {α : Type u_2} [GeneralizedCoheytingAlgebra α] {a : α} {b : α} : a \ b ≤ b ↔ a ≤ b

@[simp]

theorem sdiff_self {α : Type u_2} [GeneralizedCoheytingAlgebra α] {a : α} : a \ a = ⊥

theorem le_sup_sdiff {α : Type u_2} [GeneralizedCoheytingAlgebra α] {a : α} {b : α} : a ≤ b ⊔ a \ b

theorem le_sdiff_sup {α : Type u_2} [GeneralizedCoheytingAlgebra α] {a : α} {b : α} : a ≤ a \ b ⊔ b

theorem sup_sdiff_left {α : Type u_2} [GeneralizedCoheytingAlgebra α] {a : α} {b : α} : a ⊔ a \ b = a

theorem sup_sdiff_right {α : Type u_2} [GeneralizedCoheytingAlgebra α] {a : α} {b : α} : a \ b ⊔ a = a

theorem inf_sdiff_left {α : Type u_2} [GeneralizedCoheytingAlgebra α] {a : α} {b : α} : a \ b ⊓ a = a \ b

theorem inf_sdiff_right {α : Type u_2} [GeneralizedCoheytingAlgebra α] {a : α} {b : α} : a ⊓ a \ b = a \ b

@[simp]

theorem sup_sdiff_self {α : Type u_2} [GeneralizedCoheytingAlgebra α] (a : α) (b : α) : a ⊔ b \ a = a ⊔ b

@[simp]

theorem sdiff_sup_self {α : Type u_2} [GeneralizedCoheytingAlgebra α] (a : α) (b : α) : b \ a ⊔ a = b ⊔ a

theorem sup_sdiff_self_left {α : Type u_2} [GeneralizedCoheytingAlgebra α] (a : α) (b : α) : b \ a ⊔ a = b ⊔ a

Alias of sdiff_sup_self.

theorem sup_sdiff_self_right {α : Type u_2} [GeneralizedCoheytingAlgebra α] (a : α) (b : α) : a ⊔ b \ a = a ⊔ b

Alias of sup_sdiff_self.

theorem sup_sdiff_eq_sup {α : Type u_2} [GeneralizedCoheytingAlgebra α] {a : α} {b : α} {c : α} (h : c ≤ a) : a ⊔ b \ c = a ⊔ b

theorem sup_sdiff_cancel' {α : Type u_2} [GeneralizedCoheytingAlgebra α] {a : α} {b : α} {c : α} (hab : a ≤ b) (hbc : b ≤ c) : b ⊔ c \ a = c

theorem sup_sdiff_cancel_right {α : Type u_2} [GeneralizedCoheytingAlgebra α] {a : α} {b : α} (h : a ≤ b) : a ⊔ b \ a = b

theorem sdiff_sup_cancel {α : Type u_2} [GeneralizedCoheytingAlgebra α] {a : α} {b : α} (h : b ≤ a) : a \ b ⊔ b = a

theorem sup_le_of_le_sdiff_left {α : Type u_2} [GeneralizedCoheytingAlgebra α] {a : α} {b : α} {c : α} (h : b ≤ c \ a) (hac : a ≤ c) : a ⊔ b ≤ c

theorem sup_le_of_le_sdiff_right {α : Type u_2} [GeneralizedCoheytingAlgebra α] {a : α} {b : α} {c : α} (h : a ≤ c \ b) (hbc : b ≤ c) : a ⊔ b ≤ c

@[simp]

theorem sdiff_eq_bot_iff {α : Type u_2} [GeneralizedCoheytingAlgebra α] {a : α} {b : α} : a \ b = ⊥ ↔ a ≤ b

@[simp]

theorem sdiff_bot {α : Type u_2} [GeneralizedCoheytingAlgebra α] {a : α} : a \ ⊥ = a

@[simp]

theorem bot_sdiff {α : Type u_2} [GeneralizedCoheytingAlgebra α] {a : α} : ⊥ \ a = ⊥

theorem sdiff_sdiff_sdiff_le_sdiff {α : Type u_2} [GeneralizedCoheytingAlgebra α] {a : α} {b : α} {c : α} : (a \ b) \ (a \ c) ≤ c \ b

@[simp]

theorem le_sup_sdiff_sup_sdiff {α : Type u_2} [GeneralizedCoheytingAlgebra α] {a : α} {b : α} {c : α} : a ≤ b ⊔ (a \ c ⊔ c \ b)

theorem sdiff_sdiff {α : Type u_2} [GeneralizedCoheytingAlgebra α] (a : α) (b : α) (c : α) : (a \ b) \ c = a \ (b ⊔ c)

theorem sdiff_sdiff_left {α : Type u_2} [GeneralizedCoheytingAlgebra α] {a : α} {b : α} {c : α} : (a \ b) \ c = a \ (b ⊔ c)

theorem sdiff_right_comm {α : Type u_2} [GeneralizedCoheytingAlgebra α] (a : α) (b : α) (c : α) : (a \ b) \ c = (a \ c) \ b

theorem sdiff_sdiff_comm {α : Type u_2} [GeneralizedCoheytingAlgebra α] {a : α} {b : α} {c : α} : (a \ b) \ c = (a \ c) \ b

@[simp]

theorem sdiff_idem {α : Type u_2} [GeneralizedCoheytingAlgebra α] {a : α} {b : α} : (a \ b) \ b = a \ b

@[simp]

theorem sdiff_sdiff_self {α : Type u_2} [GeneralizedCoheytingAlgebra α] {a : α} {b : α} : (a \ b) \ a = ⊥

theorem sup_sdiff_distrib {α : Type u_2} [GeneralizedCoheytingAlgebra α] (a : α) (b : α) (c : α) : (a ⊔ b) \ c = a \ c ⊔ b \ c

theorem sdiff_inf_distrib {α : Type u_2} [GeneralizedCoheytingAlgebra α] (a : α) (b : α) (c : α) : a \ (b ⊓ c) = a \ b ⊔ a \ c

theorem sup_sdiff {α : Type u_2} [GeneralizedCoheytingAlgebra α] {a : α} {b : α} {c : α} : (a ⊔ b) \ c = a \ c ⊔ b \ c

@[simp]

theorem sup_sdiff_right_self {α : Type u_2} [GeneralizedCoheytingAlgebra α] {a : α} {b : α} : (a ⊔ b) \ b = a \ b

@[simp]

theorem sup_sdiff_left_self {α : Type u_2} [GeneralizedCoheytingAlgebra α] {a : α} {b : α} : (a ⊔ b) \ a = b \ a

theorem sdiff_le_sdiff_right {α : Type u_2} [GeneralizedCoheytingAlgebra α] {a : α} {b : α} {c : α} (h : a ≤ b) : a \ c ≤ b \ c

theorem sdiff_le_sdiff_left {α : Type u_2} [GeneralizedCoheytingAlgebra α] {a : α} {b : α} {c : α} (h : a ≤ b) : c \ b ≤ c \ a

theorem sdiff_le_sdiff {α : Type u_2} [GeneralizedCoheytingAlgebra α] {a : α} {b : α} {c : α} {d : α} (hab : a ≤ b) (hcd : c ≤ d) : a \ d ≤ b \ c

theorem sdiff_inf {α : Type u_2} [GeneralizedCoheytingAlgebra α] {a : α} {b : α} {c : α} : a \ (b ⊓ c) = a \ b ⊔ a \ c

@[simp]

theorem sdiff_inf_self_left {α : Type u_2} [GeneralizedCoheytingAlgebra α] (a : α) (b : α) : a \ (a ⊓ b) = a \ b

@[simp]

theorem sdiff_inf_self_right {α : Type u_2} [GeneralizedCoheytingAlgebra α] (a : α) (b : α) : b \ (a ⊓ b) = b \ a

theorem Disjoint.sdiff_eq_left {α : Type u_2} [GeneralizedCoheytingAlgebra α] {a : α} {b : α} (h : Disjoint a b) : a \ b = a

theorem Disjoint.sdiff_eq_right {α : Type u_2} [GeneralizedCoheytingAlgebra α] {a : α} {b : α} (h : Disjoint a b) : b \ a = b

theorem Disjoint.sup_sdiff_cancel_left {α : Type u_2} [GeneralizedCoheytingAlgebra α] {a : α} {b : α} (h : Disjoint a b) : (a ⊔ b) \ a = b

theorem Disjoint.sup_sdiff_cancel_right {α : Type u_2} [GeneralizedCoheytingAlgebra α] {a : α} {b : α} (h : Disjoint a b) : (a ⊔ b) \ b = a

theorem Disjoint.le_sdiff_of_le_left {α : Type u_2} [GeneralizedCoheytingAlgebra α] {a : α} {b : α} {c : α} (hac : Disjoint a c) (hab : a ≤ b) : a ≤ b \ c

See le_sdiff for a stronger version in generalised Boolean algebras.

theorem sdiff_sdiff_le {α : Type u_2} [GeneralizedCoheytingAlgebra α] {a : α} {b : α} : a \ (a \ b) ≤ b

@[simp]

theorem sdiff_eq_sdiff_iff {α : Type u_2} [GeneralizedCoheytingAlgebra α] {a : α} {b : α} : a \ b = b \ a ↔ a = b

theorem sdiff_ne_sdiff_iff {α : Type u_2} [GeneralizedCoheytingAlgebra α] {a : α} {b : α} : a \ b ≠ b \ a ↔ a ≠ b

theorem sdiff_triangle {α : Type u_2} [GeneralizedCoheytingAlgebra α] (a : α) (b : α) (c : α) : a \ c ≤ a \ b ⊔ b \ c

theorem sdiff_sup_sdiff_cancel {α : Type u_2} [GeneralizedCoheytingAlgebra α] {a : α} {b : α} {c : α} (hba : b ≤ a) (hcb : c ≤ b) : a \ b ⊔ b \ c = a \ c

theorem sdiff_le_sdiff_of_sup_le_sup_left {α : Type u_2} [GeneralizedCoheytingAlgebra α] {a : α} {b : α} {c : α} (h : c ⊔ a ≤ c ⊔ b) : a \ c ≤ b \ c

theorem sdiff_le_sdiff_of_sup_le_sup_right {α : Type u_2} [GeneralizedCoheytingAlgebra α] {a : α} {b : α} {c : α} (h : a ⊔ c ≤ b ⊔ c) : a \ c ≤ b \ c

@[simp]

theorem inf_sdiff_sup_left {α : Type u_2} [GeneralizedCoheytingAlgebra α] {a : α} {b : α} {c : α} : a \ c ⊓ (a ⊔ b) = a \ c

@[simp]

theorem inf_sdiff_sup_right {α : Type u_2} [GeneralizedCoheytingAlgebra α] {a : α} {b : α} {c : α} : a \ c ⊓ (b ⊔ a) = a \ c

@[instance 100]

instance GeneralizedCoheytingAlgebra.toDistribLattice {α : Type u_2} [GeneralizedCoheytingAlgebra α] : DistribLattice α

Equations

• GeneralizedCoheytingAlgebra.toDistribLattice = DistribLattice.mk ⋯

instance OrderDual.instGeneralizedHeytingAlgebra {α : Type u_2} [GeneralizedCoheytingAlgebra α] : GeneralizedHeytingAlgebra αᵒᵈ

Equations

• OrderDual.instGeneralizedHeytingAlgebra = GeneralizedHeytingAlgebra.mk ⋯

instance Prod.instGeneralizedCoheytingAlgebra {α : Type u_2} {β : Type u_3} [GeneralizedCoheytingAlgebra α] [GeneralizedCoheytingAlgebra β] : GeneralizedCoheytingAlgebra (α × β)

Equations

• Prod.instGeneralizedCoheytingAlgebra = GeneralizedCoheytingAlgebra.mk ⋯

instance Pi.instGeneralizedCoheytingAlgebra {ι : Type u_1} {α : ι → Type u_4} [(i : ι) → GeneralizedCoheytingAlgebra (α i)] : GeneralizedCoheytingAlgebra ((i : ι) → α i)

Equations

• Pi.instGeneralizedCoheytingAlgebra = GeneralizedCoheytingAlgebra.mk ⋯

@[simp]

theorem himp_bot {α : Type u_2} [HeytingAlgebra α] (a : α) : a ⇨ ⊥ = aᶜ

@[simp]

theorem bot_himp {α : Type u_2} [HeytingAlgebra α] (a : α) : ⊥ ⇨ a = ⊤

theorem compl_sup_distrib {α : Type u_2} [HeytingAlgebra α] (a : α) (b : α) : (a ⊔ b)ᶜ = aᶜ ⊓ bᶜ

@[simp]

theorem compl_sup {α : Type u_2} [HeytingAlgebra α] {a : α} {b : α} : (a ⊔ b)ᶜ = aᶜ ⊓ bᶜ

theorem compl_le_himp {α : Type u_2} [HeytingAlgebra α] {a : α} {b : α} : aᶜ ≤ a ⇨ b

theorem compl_sup_le_himp {α : Type u_2} [HeytingAlgebra α] {a : α} {b : α} : aᶜ ⊔ b ≤ a ⇨ b

theorem sup_compl_le_himp {α : Type u_2} [HeytingAlgebra α] {a : α} {b : α} : b ⊔ aᶜ ≤ a ⇨ b

@[simp]

theorem himp_compl {α : Type u_2} [HeytingAlgebra α] (a : α) : a ⇨ aᶜ = aᶜ

theorem himp_compl_comm {α : Type u_2} [HeytingAlgebra α] (a : α) (b : α) : a ⇨ bᶜ = b ⇨ aᶜ

theorem le_compl_iff_disjoint_right {α : Type u_2} [HeytingAlgebra α] {a : α} {b : α} : a ≤ bᶜ ↔ Disjoint a b

theorem le_compl_iff_disjoint_left {α : Type u_2} [HeytingAlgebra α] {a : α} {b : α} : a ≤ bᶜ ↔ Disjoint b a

theorem le_compl_comm {α : Type u_2} [HeytingAlgebra α] {a : α} {b : α} : a ≤ bᶜ ↔ b ≤ aᶜ

theorem Disjoint.le_compl_right {α : Type u_2} [HeytingAlgebra α] {a : α} {b : α} : Disjoint a b → a ≤ bᶜ

Alias of the reverse direction of le_compl_iff_disjoint_right.

theorem Disjoint.le_compl_left {α : Type u_2} [HeytingAlgebra α] {a : α} {b : α} : Disjoint b a → a ≤ bᶜ

Alias of the reverse direction of le_compl_iff_disjoint_left.

theorem le_compl_iff_le_compl {α : Type u_2} [HeytingAlgebra α] {a : α} {b : α} : a ≤ bᶜ ↔ b ≤ aᶜ

Alias of le_compl_comm.

theorem le_compl_of_le_compl {α : Type u_2} [HeytingAlgebra α] {a : α} {b : α} : a ≤ bᶜ → b ≤ aᶜ

Alias of the forward direction of le_compl_comm.

theorem disjoint_compl_left {α : Type u_2} [HeytingAlgebra α] {a : α} : Disjoint aᶜ a

theorem disjoint_compl_right {α : Type u_2} [HeytingAlgebra α] {a : α} : Disjoint a aᶜ

theorem LE.le.disjoint_compl_left {α : Type u_2} [HeytingAlgebra α] {a : α} {b : α} (h : b ≤ a) : Disjoint aᶜ b

theorem LE.le.disjoint_compl_right {α : Type u_2} [HeytingAlgebra α] {a : α} {b : α} (h : a ≤ b) : Disjoint a bᶜ

theorem IsCompl.compl_eq {α : Type u_2} [HeytingAlgebra α] {a : α} {b : α} (h : IsCompl a b) : aᶜ = b

theorem IsCompl.eq_compl {α : Type u_2} [HeytingAlgebra α] {a : α} {b : α} (h : IsCompl a b) : a = bᶜ

theorem compl_unique {α : Type u_2} [HeytingAlgebra α] {a : α} {b : α} (h₀ : a ⊓ b = ⊥) (h₁ : a ⊔ b = ⊤) : aᶜ = b

@[simp]

theorem inf_compl_self {α : Type u_2} [HeytingAlgebra α] (a : α) : a ⊓ aᶜ = ⊥

@[simp]

theorem compl_inf_self {α : Type u_2} [HeytingAlgebra α] (a : α) : aᶜ ⊓ a = ⊥

theorem inf_compl_eq_bot {α : Type u_2} [HeytingAlgebra α] {a : α} : a ⊓ aᶜ = ⊥

theorem compl_inf_eq_bot {α : Type u_2} [HeytingAlgebra α] {a : α} : aᶜ ⊓ a = ⊥

@[simp]

theorem compl_top {α : Type u_2} [HeytingAlgebra α] : ⊤ᶜ = ⊥

@[simp]

theorem compl_bot {α : Type u_2} [HeytingAlgebra α] : ⊥ᶜ = ⊤

@[simp]

theorem le_compl_self {α : Type u_2} [HeytingAlgebra α] {a : α} : a ≤ aᶜ ↔ a = ⊥

@[simp]

theorem ne_compl_self {α : Type u_2} [HeytingAlgebra α] {a : α} [Nontrivial α] : a ≠ aᶜ

@[simp]

theorem compl_ne_self {α : Type u_2} [HeytingAlgebra α] {a : α} [Nontrivial α] : aᶜ ≠ a

@[simp]

theorem lt_compl_self {α : Type u_2} [HeytingAlgebra α] {a : α} [Nontrivial α] : a < aᶜ ↔ a = ⊥

theorem le_compl_compl {α : Type u_2} [HeytingAlgebra α] {a : α} : a ≤ aᶜᶜ

theorem compl_anti {α : Type u_2} [HeytingAlgebra α] : Antitone compl

theorem compl_le_compl {α : Type u_2} [HeytingAlgebra α] {a : α} {b : α} (h : a ≤ b) : bᶜ ≤ aᶜ

@[simp]

theorem compl_compl_compl {α : Type u_2} [HeytingAlgebra α] (a : α) : aᶜᶜᶜ = aᶜ

@[simp]

theorem disjoint_compl_compl_left_iff {α : Type u_2} [HeytingAlgebra α] {a : α} {b : α} : Disjoint aᶜᶜ b ↔ Disjoint a b

@[simp]

theorem disjoint_compl_compl_right_iff {α : Type u_2} [HeytingAlgebra α] {a : α} {b : α} : Disjoint a bᶜᶜ ↔ Disjoint a b

theorem compl_sup_compl_le {α : Type u_2} [HeytingAlgebra α] {a : α} {b : α} : aᶜ ⊔ bᶜ ≤ (a ⊓ b)ᶜ

theorem compl_compl_inf_distrib {α : Type u_2} [HeytingAlgebra α] (a : α) (b : α) : (a ⊓ b)ᶜᶜ = aᶜᶜ ⊓ bᶜᶜ

theorem compl_compl_himp_distrib {α : Type u_2} [HeytingAlgebra α] (a : α) (b : α) : (a ⇨ b)ᶜᶜ = aᶜᶜ ⇨ bᶜᶜ

instance OrderDual.instCoheytingAlgebra {α : Type u_2} [HeytingAlgebra α] : CoheytingAlgebra αᵒᵈ

Equations

• OrderDual.instCoheytingAlgebra = CoheytingAlgebra.mk ⋯

@[simp]

theorem ofDual_hnot {α : Type u_2} [HeytingAlgebra α] (a : αᵒᵈ) : OrderDual.ofDual (￢a) = (OrderDual.ofDual a)ᶜ

@[simp]

theorem toDual_compl {α : Type u_2} [HeytingAlgebra α] (a : α) : OrderDual.toDual aᶜ = ￢OrderDual.toDual a

instance Prod.instHeytingAlgebra {α : Type u_2} {β : Type u_3} [HeytingAlgebra α] [HeytingAlgebra β] : HeytingAlgebra (α × β)

Equations

• Prod.instHeytingAlgebra = HeytingAlgebra.mk ⋯

instance Pi.instHeytingAlgebra {ι : Type u_1} {α : ι → Type u_4} [(i : ι) → HeytingAlgebra (α i)] : HeytingAlgebra ((i : ι) → α i)

Equations

• Pi.instHeytingAlgebra = HeytingAlgebra.mk ⋯

@[simp]

theorem top_sdiff' {α : Type u_2} [CoheytingAlgebra α] (a : α) : ⊤ \ a = ￢a

@[simp]

theorem sdiff_top {α : Type u_2} [CoheytingAlgebra α] (a : α) : a \ ⊤ = ⊥

theorem hnot_inf_distrib {α : Type u_2} [CoheytingAlgebra α] (a : α) (b : α) : ￢(a ⊓ b) = ￢a ⊔ ￢b

theorem sdiff_le_hnot {α : Type u_2} [CoheytingAlgebra α] {a : α} {b : α} : a \ b ≤ ￢b

theorem sdiff_le_inf_hnot {α : Type u_2} [CoheytingAlgebra α] {a : α} {b : α} : a \ b ≤ a ⊓ ￢b

@[instance 100]

instance CoheytingAlgebra.toDistribLattice {α : Type u_2} [CoheytingAlgebra α] : DistribLattice α

Equations

• CoheytingAlgebra.toDistribLattice = DistribLattice.mk ⋯

@[simp]

theorem hnot_sdiff {α : Type u_2} [CoheytingAlgebra α] (a : α) : ￢a \ a = ￢a

theorem hnot_sdiff_comm {α : Type u_2} [CoheytingAlgebra α] (a : α) (b : α) : ￢a \ b = ￢b \ a

theorem hnot_le_iff_codisjoint_right {α : Type u_2} [CoheytingAlgebra α] {a : α} {b : α} : ￢a ≤ b ↔ Codisjoint a b

theorem hnot_le_iff_codisjoint_left {α : Type u_2} [CoheytingAlgebra α] {a : α} {b : α} : ￢a ≤ b ↔ Codisjoint b a

theorem hnot_le_comm {α : Type u_2} [CoheytingAlgebra α] {a : α} {b : α} : ￢a ≤ b ↔ ￢b ≤ a

theorem Codisjoint.hnot_le_right {α : Type u_2} [CoheytingAlgebra α] {a : α} {b : α} : Codisjoint a b → ￢a ≤ b

Alias of the reverse direction of hnot_le_iff_codisjoint_right.

theorem Codisjoint.hnot_le_left {α : Type u_2} [CoheytingAlgebra α] {a : α} {b : α} : Codisjoint b a → ￢a ≤ b

Alias of the reverse direction of hnot_le_iff_codisjoint_left.

theorem codisjoint_hnot_right {α : Type u_2} [CoheytingAlgebra α] {a : α} : Codisjoint a (￢a)

theorem codisjoint_hnot_left {α : Type u_2} [CoheytingAlgebra α] {a : α} : Codisjoint (￢a) a

theorem LE.le.codisjoint_hnot_left {α : Type u_2} [CoheytingAlgebra α] {a : α} {b : α} (h : a ≤ b) : Codisjoint (￢a) b

theorem LE.le.codisjoint_hnot_right {α : Type u_2} [CoheytingAlgebra α] {a : α} {b : α} (h : b ≤ a) : Codisjoint a (￢b)

theorem IsCompl.hnot_eq {α : Type u_2} [CoheytingAlgebra α] {a : α} {b : α} (h : IsCompl a b) : ￢a = b

theorem IsCompl.eq_hnot {α : Type u_2} [CoheytingAlgebra α] {a : α} {b : α} (h : IsCompl a b) : a = ￢b

@[simp]

theorem sup_hnot_self {α : Type u_2} [CoheytingAlgebra α] (a : α) : a ⊔ ￢a = ⊤

@[simp]

theorem hnot_sup_self {α : Type u_2} [CoheytingAlgebra α] (a : α) : ￢a ⊔ a = ⊤

@[simp]

theorem hnot_bot {α : Type u_2} [CoheytingAlgebra α] : ￢⊥ = ⊤

@[simp]

theorem hnot_top {α : Type u_2} [CoheytingAlgebra α] : ￢⊤ = ⊥

theorem hnot_hnot_le {α : Type u_2} [CoheytingAlgebra α] {a : α} : ￢￢a ≤ a

theorem hnot_anti {α : Type u_2} [CoheytingAlgebra α] : Antitone hnot

theorem hnot_le_hnot {α : Type u_2} [CoheytingAlgebra α] {a : α} {b : α} (h : a ≤ b) : ￢b ≤ ￢a

@[simp]

theorem hnot_hnot_hnot {α : Type u_2} [CoheytingAlgebra α] (a : α) : ￢￢￢a = ￢a

@[simp]

theorem codisjoint_hnot_hnot_left_iff {α : Type u_2} [CoheytingAlgebra α] {a : α} {b : α} : Codisjoint (￢￢a) b ↔ Codisjoint a b

@[simp]

theorem codisjoint_hnot_hnot_right_iff {α : Type u_2} [CoheytingAlgebra α] {a : α} {b : α} : Codisjoint a (￢￢b) ↔ Codisjoint a b

theorem le_hnot_inf_hnot {α : Type u_2} [CoheytingAlgebra α] {a : α} {b : α} : ￢(a ⊔ b) ≤ ￢a ⊓ ￢b

theorem hnot_hnot_sup_distrib {α : Type u_2} [CoheytingAlgebra α] (a : α) (b : α) : ￢￢(a ⊔ b) = ￢￢a ⊔ ￢￢b

theorem hnot_hnot_sdiff_distrib {α : Type u_2} [CoheytingAlgebra α] (a : α) (b : α) : ￢￢(a \ b) = ￢￢a \ ￢￢b

instance OrderDual.instHeytingAlgebra {α : Type u_2} [CoheytingAlgebra α] : HeytingAlgebra αᵒᵈ

Equations

• OrderDual.instHeytingAlgebra = HeytingAlgebra.mk ⋯

@[simp]

theorem ofDual_compl {α : Type u_2} [CoheytingAlgebra α] (a : αᵒᵈ) : OrderDual.ofDual aᶜ = ￢OrderDual.ofDual a

@[simp]

theorem ofDual_himp {α : Type u_2} [CoheytingAlgebra α] (a : αᵒᵈ) (b : αᵒᵈ) : OrderDual.ofDual (a ⇨ b) = OrderDual.ofDual b \ OrderDual.ofDual a

@[simp]

theorem toDual_hnot {α : Type u_2} [CoheytingAlgebra α] (a : α) : OrderDual.toDual (￢a) = (OrderDual.toDual a)ᶜ

@[simp]

theorem toDual_sdiff {α : Type u_2} [CoheytingAlgebra α] (a : α) (b : α) : OrderDual.toDual (a \ b) = OrderDual.toDual b ⇨ OrderDual.toDual a

instance Prod.instCoheytingAlgebra {α : Type u_2} {β : Type u_3} [CoheytingAlgebra α] [CoheytingAlgebra β] : CoheytingAlgebra (α × β)

Equations

• Prod.instCoheytingAlgebra = CoheytingAlgebra.mk ⋯

instance Pi.instCoheytingAlgebra {ι : Type u_1} {α : ι → Type u_4} [(i : ι) → CoheytingAlgebra (α i)] : CoheytingAlgebra ((i : ι) → α i)

Equations

• Pi.instCoheytingAlgebra = CoheytingAlgebra.mk ⋯

theorem compl_le_hnot {α : Type u_2} [BiheytingAlgebra α] {a : α} : aᶜ ≤ ￢a

instance Prop.instHeytingAlgebra : HeytingAlgebra Prop

Propositions form a Heyting algebra with implication as Heyting implication and negation as complement.

Equations

• «Prop».instHeytingAlgebra = HeytingAlgebra.mk «Prop».instHeytingAlgebra.proof_2

@[simp]

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

@[simp]

theorem compl_iff_not (p : Prop) : pᶜ ↔ ¬p

@[reducible, inline]

abbrev LinearOrder.toBiheytingAlgebra {α : Type u_2} [LinearOrder α] [BoundedOrder α] : BiheytingAlgebra α

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.

Equations

• LinearOrder.toBiheytingAlgebra = BiheytingAlgebra.mk ⋯ ⋯

instance OrderDual.instBiheytingAlgebra {α : Type u_2} [BiheytingAlgebra α] : BiheytingAlgebra αᵒᵈ

Equations

• OrderDual.instBiheytingAlgebra = BiheytingAlgebra.mk ⋯ ⋯

instance Prod.instBiheytingAlgebra {α : Type u_2} {β : Type u_3} [BiheytingAlgebra α] [BiheytingAlgebra β] : BiheytingAlgebra (α × β)

Equations

• Prod.instBiheytingAlgebra = BiheytingAlgebra.mk ⋯ ⋯

instance Pi.instBiheytingAlgebra {ι : Type u_1} {α : ι → Type u_4} [(i : ι) → BiheytingAlgebra (α i)] : BiheytingAlgebra ((i : ι) → α i)

Equations

• Pi.instBiheytingAlgebra = BiheytingAlgebra.mk ⋯ ⋯

@[reducible, inline]

abbrev Function.Injective.generalizedHeytingAlgebra {α : Type u_2} {β : Type u_3} [Sup α] [Inf α] [Top α] [HImp α] [GeneralizedHeytingAlgebra β] (f : α → β) (hf : Function.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 α

Pullback a GeneralizedHeytingAlgebra along an injection.

Equations

• Function.Injective.generalizedHeytingAlgebra f hf map_sup map_inf map_top map_himp = GeneralizedHeytingAlgebra.mk ⋯

@[reducible, inline]

abbrev Function.Injective.generalizedCoheytingAlgebra {α : Type u_2} {β : Type u_3} [Sup α] [Inf α] [Bot α] [SDiff α] [GeneralizedCoheytingAlgebra β] (f : α → β) (hf : Function.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 α

Pullback a GeneralizedCoheytingAlgebra along an injection.

Equations

• Function.Injective.generalizedCoheytingAlgebra f hf map_sup map_inf map_bot map_sdiff = GeneralizedCoheytingAlgebra.mk ⋯

@[reducible, inline]

abbrev Function.Injective.heytingAlgebra {α : Type u_2} {β : Type u_3} [Sup α] [Inf α] [Top α] [Bot α] [HasCompl α] [HImp α] [HeytingAlgebra β] (f : α → β) (hf : Function.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 α

Pullback a HeytingAlgebra along an injection.

Equations

• Function.Injective.heytingAlgebra f hf map_sup map_inf map_top map_bot map_compl map_himp = HeytingAlgebra.mk ⋯

@[reducible, inline]

abbrev Function.Injective.coheytingAlgebra {α : Type u_2} {β : Type u_3} [Sup α] [Inf α] [Top α] [Bot α] [HNot α] [SDiff α] [CoheytingAlgebra β] (f : α → β) (hf : Function.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 α

Pullback a CoheytingAlgebra along an injection.

Equations

• Function.Injective.coheytingAlgebra f hf map_sup map_inf map_top map_bot map_hnot map_sdiff = CoheytingAlgebra.mk ⋯

@[reducible, inline]

abbrev Function.Injective.biheytingAlgebra {α : Type u_2} {β : Type u_3} [Sup α] [Inf α] [Top α] [Bot α] [HasCompl α] [HNot α] [HImp α] [SDiff α] [BiheytingAlgebra β] (f : α → β) (hf : Function.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 α

Pullback a BiheytingAlgebra along an injection.

Equations

• Function.Injective.biheytingAlgebra f hf map_sup map_inf map_top map_bot map_compl map_hnot map_himp map_sdiff = BiheytingAlgebra.mk ⋯ ⋯

instance PUnit.instBiheytingAlgebra : BiheytingAlgebra PUnit.{u + 1}

Equations

• PUnit.instBiheytingAlgebra = BiheytingAlgebra.mk PUnit.instBiheytingAlgebra.proof_3 PUnit.instBiheytingAlgebra.proof_4

@[simp]

theorem PUnit.top_eq : ⊤ = PUnit.unit

@[simp]

theorem PUnit.bot_eq : ⊥ = PUnit.unit

@[simp]

theorem PUnit.sup_eq (a : PUnit.{u + 1} ) (b : PUnit.{u + 1} ) : a ⊔ b = PUnit.unit

@[simp]

theorem PUnit.inf_eq (a : PUnit.{u + 1} ) (b : PUnit.{u + 1} ) : a ⊓ b = PUnit.unit

@[simp]

theorem PUnit.compl_eq (a : PUnit.{u + 1} ) : aᶜ = PUnit.unit

@[simp]

theorem PUnit.sdiff_eq (a : PUnit.{u + 1} ) (b : PUnit.{u + 1} ) : a \ b = PUnit.unit

@[simp]

theorem PUnit.hnot_eq (a : PUnit.{u + 1} ) : ￢a = PUnit.unit

@[simp]

theorem PUnit.himp_eq (a : PUnit.{u + 1} ) (b : PUnit.{u + 1} ) : a ⇨ b = PUnit.unit