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.

Notation

• ⇨: Heyting implication
• \: Difference
• ￢: Heyting negation
• ᶜ: (Pseudo-)complement

References

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

Tags

Heyting, Brouwer, algebra, implication, negation, intuitionistic

Notation

class HImp (α : Type u_4) : Type u_4

Syntax typeclass for Heyting implication ⇨.

• himp : α → α → α

  Heyting implication ⇨

class HNot (α : Type u_4) : Type u_4

Syntax typeclass for Heyting negation ￢.

The difference between HasCompl and HNot is that the former belongs to Heyting algebras, while the latter belongs to co-Heyting algebras. They are both pseudo-complements, but compl underestimates while HNot overestimates. In boolean algebras, they are equal. See hnot_eq_compl.

• hnot : α → α

  Heyting negation ￢

def «term_⇨_» : Lean.TrailingParserDescr

Heyting implication

Equations

• «term_⇨_» = Lean.ParserDescr.trailingNode `term_⇨_ 60 61 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⇨ ") (Lean.ParserDescr.cat `term 60))

def «term￢_» : Lean.ParserDescr

Heyting negation

Equations

• «term￢_» = Lean.ParserDescr.node `term￢_ 72 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "￢") (Lean.ParserDescr.cat `term 72))

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

• Prod.hasCompl α β = { 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 ⊓

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

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 right adjoint to 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

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

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

Equations

• HeytingAlgebra.toBoundedOrder = BoundedOrder.mk

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

Equations

• CoheytingAlgebra.toBoundedOrder = let src := inst; BoundedOrder.mk

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

Equations

• BiheytingAlgebra.toCoheytingAlgebra = let src := inst; CoheytingAlgebra.mk (_ : ∀ (a : α), ⊤ \ a = ￢a)

@[reducible]

def 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 = let src := inst✝; let src_1 := inst; HeytingAlgebra.mk (_ : ∀ (a : α), a ⇨ ⊥ = a ⇨ ⊥)

@[reducible]

def 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 = let src := inst✝; let src_1 := inst; HeytingAlgebra.mk (_ : ∀ (a : α), compl a ⊔ ⊥ = compl a)

@[reducible]

def 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 = let src := inst✝; let src_1 := inst; CoheytingAlgebra.mk (_ : ∀ (a : α), ⊤ \ a = ⊤ \ a)

@[reducible]

def 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 = let src := inst✝; let src_1 := inst; CoheytingAlgebra.mk (_ : ∀ (a : α), ⊤ ⊓ hnot a = hnot a)

@[simp]

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

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

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

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

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

@[simp]

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

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

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

@[simp]

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

@[simp]

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

@[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 ⇨ ⊤ = ⊤

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

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

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

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

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 GeneralizedHeytingAlgebra.toDistribLattice {α : Type u_2} [GeneralizedHeytingAlgebra α] : DistribLattice α

Equations

• GeneralizedHeytingAlgebra.toDistribLattice = DistribLattice.ofInfSupLe (_ : ∀ (a b c : α), a ⊓ (b ⊔ c) ≤ a ⊓ b ⊔ a ⊓ c)

instance instGeneralizedCoheytingAlgebraOrderDual {α : Type u_2} [GeneralizedHeytingAlgebra α] : GeneralizedCoheytingAlgebra αᵒᵈ

Equations

• instGeneralizedCoheytingAlgebraOrderDual = let src := OrderDual.lattice α; let src_1 := OrderDual.orderBot α; GeneralizedCoheytingAlgebra.mk (_ : ∀ (a b c : αᵒᵈ), a \ b ≤ c ↔ a ≤ b ⊔ c)

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• Pi.generalizedHeytingAlgebra = let src := Pi.lattice; let src_1 := Pi.orderTop; GeneralizedHeytingAlgebra.mk (_ : ∀ (i a a_1 : (i : ι) → α i), i ≤ a ⇨ a_1 ↔ i ⊓ a ≤ a_1)

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

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 GeneralizedCoheytingAlgebra.toDistribLattice {α : Type u_2} [GeneralizedCoheytingAlgebra α] : DistribLattice α

Equations

• GeneralizedCoheytingAlgebra.toDistribLattice = let src := inst; DistribLattice.mk (_ : ∀ (a b c : α), (a ⊔ b) ⊓ (a ⊔ c) ≤ a ⊔ b ⊓ c)

instance instGeneralizedHeytingAlgebraOrderDual {α : Type u_2} [GeneralizedCoheytingAlgebra α] : GeneralizedHeytingAlgebra αᵒᵈ

Equations

• instGeneralizedHeytingAlgebraOrderDual = let src := OrderDual.lattice α; let src_1 := OrderDual.orderTop α; GeneralizedHeytingAlgebra.mk (_ : ∀ (a b c : αᵒᵈ), a ≤ b ⇨ c ↔ a ⊓ b ≤ c)

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• Pi.generalizedCoheytingAlgebra = let src := Pi.lattice; let src_1 := Pi.orderBot; GeneralizedCoheytingAlgebra.mk (_ : ∀ (i a a_1 : (i : ι) → α i), i \ a ≤ a_1 ↔ i ≤ a ⊔ a_1)

@[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 instCoheytingAlgebraOrderDual {α : Type u_2} [HeytingAlgebra α] : CoheytingAlgebra αᵒᵈ

Equations

• instCoheytingAlgebraOrderDual = let src := OrderDual.lattice α; let src_1 := OrderDual.boundedOrder α; CoheytingAlgebra.mk (_ : ∀ (a : α), a ⇨ ⊥ = aᶜ)

@[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.heytingAlgebra {α : Type u_2} {β : Type u_3} [HeytingAlgebra α] [HeytingAlgebra β] : HeytingAlgebra (α × β)

Equations

• Prod.heytingAlgebra = let src := Prod.generalizedHeytingAlgebra; let src_1 := Prod.boundedOrder α β; let src_2 := Prod.hasCompl α β; HeytingAlgebra.mk (_ : ∀ (a : α × β), a ⇨ ⊥ = aᶜ)

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

Equations

• Pi.heytingAlgebra = let src := Pi.orderBot; let src_1 := Pi.generalizedHeytingAlgebra; HeytingAlgebra.mk (_ : ∀ (f : (i : ι) → α i), f ⇨ ⊥ = fᶜ)

@[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 CoheytingAlgebra.toDistribLattice {α : Type u_2} [CoheytingAlgebra α] : DistribLattice α

Equations

• CoheytingAlgebra.toDistribLattice = let src := inst; DistribLattice.mk (_ : ∀ (a b c : α), (a ⊔ b) ⊓ (a ⊔ c) ≤ a ⊔ b ⊓ c)

@[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 instHeytingAlgebraOrderDual {α : Type u_2} [CoheytingAlgebra α] : HeytingAlgebra αᵒᵈ

Equations

• instHeytingAlgebraOrderDual = let src := OrderDual.lattice α; let src_1 := OrderDual.boundedOrder α; HeytingAlgebra.mk (_ : ∀ (a : α), ⊤ \ a = ￢a)

@[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.coheytingAlgebra {α : Type u_2} {β : Type u_3} [CoheytingAlgebra α] [CoheytingAlgebra β] : CoheytingAlgebra (α × β)

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• Pi.coheytingAlgebra = let src := Pi.orderTop; let src_1 := Pi.generalizedCoheytingAlgebra; CoheytingAlgebra.mk (_ : ∀ (f : (i : ι) → α i), ⊤ \ f = ￢f)

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

instance Prop.heytingAlgebra : HeytingAlgebra Prop

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

Equations

• Prop.heytingAlgebra = let src := Prop.distribLattice; let src_1 := Prop.boundedOrder; HeytingAlgebra.mk Prop.heytingAlgebra.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]

def 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

• One or more equations did not get rendered due to their size.

@[reducible]

def 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

• One or more equations did not get rendered due to their size.

@[reducible]

def 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

• One or more equations did not get rendered due to their size.

@[reducible]

def 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

• One or more equations did not get rendered due to their size.

@[reducible]

def 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

• One or more equations did not get rendered due to their size.

@[reducible]

def 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

• One or more equations did not get rendered due to their size.

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

Equations

• PUnit.biheytingAlgebra = let src := PUnit.linearOrder; BiheytingAlgebra.mk PUnit.biheytingAlgebra.proof_3 PUnit.biheytingAlgebra.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