# 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.

## Tags #

Heyting, Brouwer, algebra, implication, negation, intuitionistic

### Notation #

instance Prod.instHImp (α : Type u_2) (β : Type u_3) [HImp α] [HImp β] :
HImp (α × β)
Equations
• = { 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
• = { hnot := fun (a : α × β) => (a.1, a.2) }
instance Prod.instSDiff (α : Type u_2) (β : Type u_3) [] [] :
SDiff (α × β)
Equations
• = { sdiff := fun (a b : α × β) => (a.1 \ b.1, a.2 \ b.2) }
instance Prod.instHasCompl (α : Type u_2) (β : Type u_3) [] [] :
HasCompl (α × β)
Equations
• = { 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} [] [] (a : α × β) (b : α × β) :
(a \ b).1 = a.1 \ b.1
@[simp]
theorem snd_sdiff {α : Type u_2} {β : Type u_3} [] [] (a : α × β) (b : α × β) :
(a \ b).2 = a.2 \ b.2
@[simp]
theorem fst_compl {α : Type u_2} {β : Type u_3} [] [] (a : α × β) :
a.1 = a.1
@[simp]
theorem snd_compl {α : Type u_2} {β : Type u_3} [] [] (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 , , :
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 bb ca c
• lt_iff_le_not_le : ∀ (a b : α), a < b a b ¬b a
• le_antisymm : ∀ (a b : α), a bb aa = b
• le_sup_left : ∀ (a b : α), a a b
• le_sup_right : ∀ (a b : α), b a b
• sup_le : ∀ (a b c : α), a cb ca 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 ba ca 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 ⊓

Instances
theorem GeneralizedHeytingAlgebra.le_himp_iff {α : Type u_4} [self : ] (a : α) (b : α) (c : α) :
a b c a b c

a ⇨ is right adjoint to a ⊓

class GeneralizedCoheytingAlgebra (α : Type u_4) extends , , :
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 bb ca c
• lt_iff_le_not_le : ∀ (a b : α), a < b a b ¬b a
• le_antisymm : ∀ (a b : α), a bb aa = b
• le_sup_left : ∀ (a b : α), a a b
• le_sup_right : ∀ (a b : α), b a b
• sup_le : ∀ (a b c : α), a cb ca 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 ba ca 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

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

\ a is right adjoint to ⊔ a

class HeytingAlgebra (α : Type u_4) extends , , :
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 bb ca c
• lt_iff_le_not_le : ∀ (a b : α), a < b a b ¬b a
• le_antisymm : ∀ (a b : α), a bb aa = b
• le_sup_left : ∀ (a b : α), a a b
• le_sup_right : ∀ (a b : α), b a b
• sup_le : ∀ (a b c : α), a cb ca 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 ba ca 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 ⊓

Instances
theorem HeytingAlgebra.himp_bot {α : Type u_4} [self : ] (a : α) :

a ⇨ is right adjoint to a ⊓

class CoheytingAlgebra (α : Type u_4) extends , , :
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 bb ca c
• lt_iff_le_not_le : ∀ (a b : α), a < b a b ¬b a
• le_antisymm : ∀ (a b : α), a bb aa = b
• le_sup_left : ∀ (a b : α), a a b
• le_sup_right : ∀ (a b : α), b a b
• sup_le : ∀ (a b c : α), a cb ca 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 ba ca 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

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

⊤ \ a is ￢a

class BiheytingAlgebra (α : Type u_4) extends , , :
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 bb ca c
• lt_iff_le_not_le : ∀ (a b : α), a < b a b ¬b a
• le_antisymm : ∀ (a b : α), a bb aa = b
• le_sup_left : ∀ (a b : α), a a b
• le_sup_right : ∀ (a b : α), b a b
• sup_le : ∀ (a b c : α), a cb ca 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 ba ca 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

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

\ a is right adjoint to ⊔ a

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

⊤ \ a is ￢a

@[instance 100]
instance HeytingAlgebra.toBoundedOrder {α : Type u_2} [] :
Equations
• HeytingAlgebra.toBoundedOrder = BoundedOrder.mk
@[instance 100]
instance CoheytingAlgebra.toBoundedOrder {α : Type u_2} [] :
Equations
• CoheytingAlgebra.toBoundedOrder = BoundedOrder.mk
@[instance 100]
instance BiheytingAlgebra.toCoheytingAlgebra {α : Type u_2} [] :
Equations
• BiheytingAlgebra.toCoheytingAlgebra =
@[reducible, inline]
abbrev HeytingAlgebra.ofHImp {α : Type u_2} [] [] (himp : ααα) (le_himp_iff : ∀ (a b c : α), a himp b c a b c) :

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

Equations
Instances For
@[reducible, inline]
abbrev HeytingAlgebra.ofCompl {α : Type u_2} [] [] (compl : αα) (le_himp_iff : ∀ (a b c : α), a compl b c a b c) :

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

Equations
Instances For
@[reducible, inline]
abbrev CoheytingAlgebra.ofSDiff {α : Type u_2} [] [] (sdiff : ααα) (sdiff_le_iff : ∀ (a b c : α), sdiff a b c a b c) :

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

Equations
Instances For
@[reducible, inline]
abbrev CoheytingAlgebra.ofHNot {α : Type u_2} [] [] (hnot : αα) (sdiff_le_iff : ∀ (a b c : α), a hnot b c a b c) :

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

Equations
Instances For

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} {a : α} {b : α} {c : α} :
a b c a b c

p → q → r ↔ p ∧ q → r

theorem le_himp_iff' {α : Type u_2} {a : α} {b : α} {c : α} :
a b c b a c

p → q → r ↔ q ∧ p → r

theorem le_himp_comm {α : Type u_2} {a : α} {b : α} {c : α} :
a b c b a c

p → q → r ↔ q → p → r

theorem le_himp {α : Type u_2} {a : α} {b : α} :
a b a

p → q → p

theorem le_himp_iff_left {α : Type u_2} {a : α} {b : α} :
a a b a b

p → p → q ↔ p → q

@[simp]
theorem himp_self {α : Type u_2} {a : α} :
a a =

p → p

theorem himp_inf_le {α : Type u_2} {a : α} {b : α} :
(a b) a b

(p → q) ∧ p → q

theorem inf_himp_le {α : Type u_2} {a : α} {b : α} :
a (a b) b

p ∧ (p → q) → q

@[simp]
theorem inf_himp {α : Type u_2} (a : α) (b : α) :
a (a b) = a b

p ∧ (p → q) ↔ p ∧ q

@[simp]
theorem himp_inf_self {α : Type u_2} (a : α) (b : α) :
(a b) a = b a

(p → q) ∧ p ↔ q ∧ p

@[simp]
theorem himp_eq_top_iff {α : Type u_2} {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} {a : α} :

p → true, true → p ↔ p

@[simp]
theorem top_himp {α : Type u_2} {a : α} :
a = a
theorem himp_himp {α : Type u_2} (a : α) (b : α) (c : α) :
a b c = a b c

p → q → r ↔ p ∧ q → r

theorem himp_le_himp_himp_himp {α : Type u_2} {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} {a : α} {b : α} {c : α} :
(b c) (a b) a c
theorem himp_left_comm {α : Type u_2} (a : α) (b : α) (c : α) :
a b c = b a c

p → q → r ↔ q → p → r

@[simp]
theorem himp_idem {α : Type u_2} {a : α} {b : α} :
b b a = b a
theorem himp_inf_distrib {α : Type u_2} (a : α) (b : α) (c : α) :
a b c = (a b) (a c)
theorem sup_himp_distrib {α : Type u_2} (a : α) (b : α) (c : α) :
a b c = (a c) (b c)
theorem himp_le_himp_left {α : Type u_2} {a : α} {b : α} {c : α} (h : a b) :
c a c b
theorem himp_le_himp_right {α : Type u_2} {a : α} {b : α} {c : α} (h : a b) :
b c a c
theorem himp_le_himp {α : Type u_2} {a : α} {b : α} {c : α} {d : α} (hab : a b) (hcd : c d) :
b c a d
@[simp]
theorem sup_himp_self_left {α : Type u_2} (a : α) (b : α) :
a b a = b a
@[simp]
theorem sup_himp_self_right {α : Type u_2} (a : α) (b : α) :
a b b = a b
theorem Codisjoint.himp_eq_right {α : Type u_2} {a : α} {b : α} (h : ) :
b a = a
theorem Codisjoint.himp_eq_left {α : Type u_2} {a : α} {b : α} (h : ) :
a b = b
theorem Codisjoint.himp_inf_cancel_right {α : Type u_2} {a : α} {b : α} (h : ) :
a a b = b
theorem Codisjoint.himp_inf_cancel_left {α : Type u_2} {a : α} {b : α} (h : ) :
b a b = a
theorem Codisjoint.himp_le_of_right_le {α : Type u_2} {a : α} {b : α} {c : α} (hac : ) (hba : b a) :
c b a

See himp_le for a stronger version in Boolean algebras.

theorem le_himp_himp {α : Type u_2} {a : α} {b : α} :
a (a b) b
@[simp]
theorem himp_eq_himp_iff {α : Type u_2} {a : α} {b : α} :
b a = a b a = b
theorem himp_ne_himp_iff {α : Type u_2} {a : α} {b : α} :
b a a b a b
theorem himp_triangle {α : Type u_2} (a : α) (b : α) (c : α) :
(a b) (b c) a c
theorem himp_inf_himp_cancel {α : Type u_2} {a : α} {b : α} {c : α} (hba : b a) (hcb : c b) :
(a b) (b c) = a c
@[instance 100]
Equations
• GeneralizedHeytingAlgebra.toDistribLattice =
Equations
• OrderDual.instGeneralizedCoheytingAlgebra =
instance Prod.instGeneralizedHeytingAlgebra {α : Type u_2} {β : Type u_3} :
Equations
• Prod.instGeneralizedHeytingAlgebra =
instance Pi.instGeneralizedHeytingAlgebra {ι : Type u_1} {α : ιType u_4} [(i : ι) → ] :
GeneralizedHeytingAlgebra ((i : ι) → α i)
Equations
• Pi.instGeneralizedHeytingAlgebra =
@[simp]
theorem sdiff_le_iff {α : Type u_2} {a : α} {b : α} {c : α} :
a \ b c a b c
theorem sdiff_le_iff' {α : Type u_2} {a : α} {b : α} {c : α} :
a \ b c a c b
theorem sdiff_le_comm {α : Type u_2} {a : α} {b : α} {c : α} :
a \ b c a \ c b
theorem sdiff_le {α : Type u_2} {a : α} {b : α} :
a \ b a
theorem Disjoint.disjoint_sdiff_left {α : Type u_2} {a : α} {b : α} {c : α} (h : Disjoint a b) :
Disjoint (a \ c) b
theorem Disjoint.disjoint_sdiff_right {α : Type u_2} {a : α} {b : α} {c : α} (h : Disjoint a b) :
Disjoint a (b \ c)
theorem sdiff_le_iff_left {α : Type u_2} {a : α} {b : α} :
a \ b b a b
@[simp]
theorem sdiff_self {α : Type u_2} {a : α} :
a \ a =
theorem le_sup_sdiff {α : Type u_2} {a : α} {b : α} :
a b a \ b
theorem le_sdiff_sup {α : Type u_2} {a : α} {b : α} :
a a \ b b
theorem sup_sdiff_left {α : Type u_2} {a : α} {b : α} :
a a \ b = a
theorem sup_sdiff_right {α : Type u_2} {a : α} {b : α} :
a \ b a = a
theorem inf_sdiff_left {α : Type u_2} {a : α} {b : α} :
a \ b a = a \ b
theorem inf_sdiff_right {α : Type u_2} {a : α} {b : α} :
a a \ b = a \ b
@[simp]
theorem sup_sdiff_self {α : Type u_2} (a : α) (b : α) :
a b \ a = a b
@[simp]
theorem sdiff_sup_self {α : Type u_2} (a : α) (b : α) :
b \ a a = b a
theorem sup_sdiff_self_left {α : Type u_2} (a : α) (b : α) :
b \ a a = b a

Alias of sdiff_sup_self.

theorem sup_sdiff_self_right {α : Type u_2} (a : α) (b : α) :
a b \ a = a b

Alias of sup_sdiff_self.

theorem sup_sdiff_eq_sup {α : Type u_2} {a : α} {b : α} {c : α} (h : c a) :
a b \ c = a b
theorem sup_sdiff_cancel' {α : Type u_2} {a : α} {b : α} {c : α} (hab : a b) (hbc : b c) :
b c \ a = c
theorem sup_sdiff_cancel_right {α : Type u_2} {a : α} {b : α} (h : a b) :
a b \ a = b
theorem sdiff_sup_cancel {α : Type u_2} {a : α} {b : α} (h : b a) :
a \ b b = a
theorem sup_le_of_le_sdiff_left {α : Type u_2} {a : α} {b : α} {c : α} (h : b c \ a) (hac : a c) :
a b c
theorem sup_le_of_le_sdiff_right {α : Type u_2} {a : α} {b : α} {c : α} (h : a c \ b) (hbc : b c) :
a b c
@[simp]
theorem sdiff_eq_bot_iff {α : Type u_2} {a : α} {b : α} :
a \ b = a b
@[simp]
theorem sdiff_bot {α : Type u_2} {a : α} :
a \ = a
@[simp]
theorem bot_sdiff {α : Type u_2} {a : α} :
theorem sdiff_sdiff_sdiff_le_sdiff {α : Type u_2} {a : α} {b : α} {c : α} :
(a \ b) \ (a \ c) c \ b
@[simp]
theorem le_sup_sdiff_sup_sdiff {α : Type u_2} {a : α} {b : α} {c : α} :
a b (a \ c c \ b)
theorem sdiff_sdiff {α : Type u_2} (a : α) (b : α) (c : α) :
(a \ b) \ c = a \ (b c)
theorem sdiff_sdiff_left {α : Type u_2} {a : α} {b : α} {c : α} :
(a \ b) \ c = a \ (b c)
theorem sdiff_right_comm {α : Type u_2} (a : α) (b : α) (c : α) :
(a \ b) \ c = (a \ c) \ b
theorem sdiff_sdiff_comm {α : Type u_2} {a : α} {b : α} {c : α} :
(a \ b) \ c = (a \ c) \ b
@[simp]
theorem sdiff_idem {α : Type u_2} {a : α} {b : α} :
(a \ b) \ b = a \ b
@[simp]
theorem sdiff_sdiff_self {α : Type u_2} {a : α} {b : α} :
(a \ b) \ a =
theorem sup_sdiff_distrib {α : Type u_2} (a : α) (b : α) (c : α) :
(a b) \ c = a \ c b \ c
theorem sdiff_inf_distrib {α : Type u_2} (a : α) (b : α) (c : α) :
a \ (b c) = a \ b a \ c
theorem sup_sdiff {α : Type u_2} {a : α} {b : α} {c : α} :
(a b) \ c = a \ c b \ c
@[simp]
theorem sup_sdiff_right_self {α : Type u_2} {a : α} {b : α} :
(a b) \ b = a \ b
@[simp]
theorem sup_sdiff_left_self {α : Type u_2} {a : α} {b : α} :
(a b) \ a = b \ a
theorem sdiff_le_sdiff_right {α : Type u_2} {a : α} {b : α} {c : α} (h : a b) :
a \ c b \ c
theorem sdiff_le_sdiff_left {α : Type u_2} {a : α} {b : α} {c : α} (h : a b) :
c \ b c \ a
theorem sdiff_le_sdiff {α : Type u_2} {a : α} {b : α} {c : α} {d : α} (hab : a b) (hcd : c d) :
a \ d b \ c
theorem sdiff_inf {α : Type u_2} {a : α} {b : α} {c : α} :
a \ (b c) = a \ b a \ c
@[simp]
theorem sdiff_inf_self_left {α : Type u_2} (a : α) (b : α) :
a \ (a b) = a \ b
@[simp]
theorem sdiff_inf_self_right {α : Type u_2} (a : α) (b : α) :
b \ (a b) = b \ a
theorem Disjoint.sdiff_eq_left {α : Type u_2} {a : α} {b : α} (h : Disjoint a b) :
a \ b = a
theorem Disjoint.sdiff_eq_right {α : Type u_2} {a : α} {b : α} (h : Disjoint a b) :
b \ a = b
theorem Disjoint.sup_sdiff_cancel_left {α : Type u_2} {a : α} {b : α} (h : Disjoint a b) :
(a b) \ a = b
theorem Disjoint.sup_sdiff_cancel_right {α : Type u_2} {a : α} {b : α} (h : Disjoint a b) :
(a b) \ b = a
theorem Disjoint.le_sdiff_of_le_left {α : Type u_2} {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} {a : α} {b : α} :
a \ (a \ b) b
@[simp]
theorem sdiff_eq_sdiff_iff {α : Type u_2} {a : α} {b : α} :
a \ b = b \ a a = b
theorem sdiff_ne_sdiff_iff {α : Type u_2} {a : α} {b : α} :
a \ b b \ a a b
theorem sdiff_triangle {α : Type u_2} (a : α) (b : α) (c : α) :
a \ c a \ b b \ c
theorem sdiff_sup_sdiff_cancel {α : Type u_2} {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} {a : α} {b : α} {c : α} (h : c a c b) :
a \ c b \ c
theorem sdiff_le_sdiff_of_sup_le_sup_right {α : Type u_2} {a : α} {b : α} {c : α} (h : a c b c) :
a \ c b \ c
@[simp]
theorem inf_sdiff_sup_left {α : Type u_2} {a : α} {b : α} {c : α} :
a \ c (a b) = a \ c
@[simp]
theorem inf_sdiff_sup_right {α : Type u_2} {a : α} {b : α} {c : α} :
a \ c (b a) = a \ c
@[instance 100]
Equations
• GeneralizedCoheytingAlgebra.toDistribLattice =
Equations
• OrderDual.instGeneralizedHeytingAlgebra =
instance Prod.instGeneralizedCoheytingAlgebra {α : Type u_2} {β : Type u_3} :
Equations
• Prod.instGeneralizedCoheytingAlgebra =
instance Pi.instGeneralizedCoheytingAlgebra {ι : Type u_1} {α : ιType u_4} [(i : ι) → ] :
GeneralizedCoheytingAlgebra ((i : ι) → α i)
Equations
• Pi.instGeneralizedCoheytingAlgebra =
@[simp]
theorem himp_bot {α : Type u_2} [] (a : α) :
@[simp]
theorem bot_himp {α : Type u_2} [] (a : α) :
theorem compl_sup_distrib {α : Type u_2} [] (a : α) (b : α) :
(a b) = a b
@[simp]
theorem compl_sup {α : Type u_2} [] {a : α} {b : α} :
(a b) = a b
theorem compl_le_himp {α : Type u_2} [] {a : α} {b : α} :
a a b
theorem compl_sup_le_himp {α : Type u_2} [] {a : α} {b : α} :
a b a b
theorem sup_compl_le_himp {α : Type u_2} [] {a : α} {b : α} :
b a a b
@[simp]
theorem himp_compl {α : Type u_2} [] (a : α) :
a a = a
theorem himp_compl_comm {α : Type u_2} [] (a : α) (b : α) :
a b = b a
theorem le_compl_iff_disjoint_right {α : Type u_2} [] {a : α} {b : α} :
theorem le_compl_iff_disjoint_left {α : Type u_2} [] {a : α} {b : α} :
theorem le_compl_comm {α : Type u_2} [] {a : α} {b : α} :
a b b a
theorem Disjoint.le_compl_right {α : Type u_2} [] {a : α} {b : α} :
Disjoint a ba b

Alias of the reverse direction of le_compl_iff_disjoint_right.

theorem Disjoint.le_compl_left {α : Type u_2} [] {a : α} {b : α} :
Disjoint b aa b

Alias of the reverse direction of le_compl_iff_disjoint_left.

theorem le_compl_iff_le_compl {α : Type u_2} [] {a : α} {b : α} :
a b b a

Alias of le_compl_comm.

theorem le_compl_of_le_compl {α : Type u_2} [] {a : α} {b : α} :
a bb a

Alias of the forward direction of le_compl_comm.

theorem disjoint_compl_left {α : Type u_2} [] {a : α} :
theorem disjoint_compl_right {α : Type u_2} [] {a : α} :
theorem LE.le.disjoint_compl_left {α : Type u_2} [] {a : α} {b : α} (h : b a) :
theorem LE.le.disjoint_compl_right {α : Type u_2} [] {a : α} {b : α} (h : a b) :
theorem IsCompl.compl_eq {α : Type u_2} [] {a : α} {b : α} (h : IsCompl a b) :
a = b
theorem IsCompl.eq_compl {α : Type u_2} [] {a : α} {b : α} (h : IsCompl a b) :
a = b
theorem compl_unique {α : Type u_2} [] {a : α} {b : α} (h₀ : a b = ) (h₁ : a b = ) :
a = b
@[simp]
theorem inf_compl_self {α : Type u_2} [] (a : α) :
@[simp]
theorem compl_inf_self {α : Type u_2} [] (a : α) :
theorem inf_compl_eq_bot {α : Type u_2} [] {a : α} :
theorem compl_inf_eq_bot {α : Type u_2} [] {a : α} :
@[simp]
theorem compl_top {α : Type u_2} [] :
@[simp]
theorem compl_bot {α : Type u_2} [] :
@[simp]
theorem le_compl_self {α : Type u_2} [] {a : α} :
a a a =
@[simp]
theorem ne_compl_self {α : Type u_2} [] {a : α} [] :
a a
@[simp]
theorem compl_ne_self {α : Type u_2} [] {a : α} [] :
a a
@[simp]
theorem lt_compl_self {α : Type u_2} [] {a : α} [] :
a < a a =
theorem le_compl_compl {α : Type u_2} [] {a : α} :
theorem compl_anti {α : Type u_2} [] :
Antitone compl
theorem compl_le_compl {α : Type u_2} [] {a : α} {b : α} (h : a b) :
@[simp]
theorem compl_compl_compl {α : Type u_2} [] (a : α) :
@[simp]
theorem disjoint_compl_compl_left_iff {α : Type u_2} [] {a : α} {b : α} :
@[simp]
theorem disjoint_compl_compl_right_iff {α : Type u_2} [] {a : α} {b : α} :
theorem compl_sup_compl_le {α : Type u_2} [] {a : α} {b : α} :
a b (a b)
theorem compl_compl_inf_distrib {α : Type u_2} [] (a : α) (b : α) :
theorem compl_compl_himp_distrib {α : Type u_2} [] (a : α) (b : α) :
instance OrderDual.instCoheytingAlgebra {α : Type u_2} [] :
Equations
• OrderDual.instCoheytingAlgebra =
@[simp]
theorem ofDual_hnot {α : Type u_2} [] (a : αᵒᵈ) :
OrderDual.ofDual (a) = (OrderDual.ofDual a)
@[simp]
theorem toDual_compl {α : Type u_2} [] (a : α) :
OrderDual.toDual a = OrderDual.toDual a
instance Prod.instHeytingAlgebra {α : Type u_2} {β : Type u_3} [] [] :
Equations
• Prod.instHeytingAlgebra =
instance Pi.instHeytingAlgebra {ι : Type u_1} {α : ιType u_4} [(i : ι) → HeytingAlgebra (α i)] :
HeytingAlgebra ((i : ι) → α i)
Equations
• Pi.instHeytingAlgebra =
@[simp]
theorem top_sdiff' {α : Type u_2} [] (a : α) :
\ a = a
@[simp]
theorem sdiff_top {α : Type u_2} [] (a : α) :
theorem hnot_inf_distrib {α : Type u_2} [] (a : α) (b : α) :
(a b) = a b
theorem sdiff_le_hnot {α : Type u_2} [] {a : α} {b : α} :
a \ b b
theorem sdiff_le_inf_hnot {α : Type u_2} [] {a : α} {b : α} :
a \ b a b
@[instance 100]
instance CoheytingAlgebra.toDistribLattice {α : Type u_2} [] :
Equations
• CoheytingAlgebra.toDistribLattice =
@[simp]
theorem hnot_sdiff {α : Type u_2} [] (a : α) :
a \ a = a
theorem hnot_sdiff_comm {α : Type u_2} [] (a : α) (b : α) :
a \ b = b \ a
theorem hnot_le_iff_codisjoint_right {α : Type u_2} [] {a : α} {b : α} :
a b
theorem hnot_le_iff_codisjoint_left {α : Type u_2} [] {a : α} {b : α} :
a b
theorem hnot_le_comm {α : Type u_2} [] {a : α} {b : α} :
a b b a
theorem Codisjoint.hnot_le_right {α : Type u_2} [] {a : α} {b : α} :
a b

Alias of the reverse direction of hnot_le_iff_codisjoint_right.

theorem Codisjoint.hnot_le_left {α : Type u_2} [] {a : α} {b : α} :
a b

Alias of the reverse direction of hnot_le_iff_codisjoint_left.

theorem codisjoint_hnot_right {α : Type u_2} [] {a : α} :
theorem codisjoint_hnot_left {α : Type u_2} [] {a : α} :
theorem LE.le.codisjoint_hnot_left {α : Type u_2} [] {a : α} {b : α} (h : a b) :
theorem LE.le.codisjoint_hnot_right {α : Type u_2} [] {a : α} {b : α} (h : b a) :
theorem IsCompl.hnot_eq {α : Type u_2} [] {a : α} {b : α} (h : IsCompl a b) :
a = b
theorem IsCompl.eq_hnot {α : Type u_2} [] {a : α} {b : α} (h : IsCompl a b) :
a = b
@[simp]
theorem sup_hnot_self {α : Type u_2} [] (a : α) :
@[simp]
theorem hnot_sup_self {α : Type u_2} [] (a : α) :
@[simp]
theorem hnot_bot {α : Type u_2} [] :
@[simp]
theorem hnot_top {α : Type u_2} [] :
theorem hnot_hnot_le {α : Type u_2} [] {a : α} :
theorem hnot_anti {α : Type u_2} [] :
theorem hnot_le_hnot {α : Type u_2} [] {a : α} {b : α} (h : a b) :
@[simp]
theorem hnot_hnot_hnot {α : Type u_2} [] (a : α) :
@[simp]
theorem codisjoint_hnot_hnot_left_iff {α : Type u_2} [] {a : α} {b : α} :
@[simp]
theorem codisjoint_hnot_hnot_right_iff {α : Type u_2} [] {a : α} {b : α} :
theorem le_hnot_inf_hnot {α : Type u_2} [] {a : α} {b : α} :
(a b) a b
theorem hnot_hnot_sup_distrib {α : Type u_2} [] (a : α) (b : α) :
theorem hnot_hnot_sdiff_distrib {α : Type u_2} [] (a : α) (b : α) :
instance OrderDual.instHeytingAlgebra {α : Type u_2} [] :
Equations
• OrderDual.instHeytingAlgebra =
@[simp]
theorem ofDual_compl {α : Type u_2} [] (a : αᵒᵈ) :
OrderDual.ofDual a = OrderDual.ofDual a
@[simp]
theorem ofDual_himp {α : Type u_2} [] (a : αᵒᵈ) (b : αᵒᵈ) :
OrderDual.ofDual (a b) = OrderDual.ofDual b \ OrderDual.ofDual a
@[simp]
theorem toDual_hnot {α : Type u_2} [] (a : α) :
OrderDual.toDual (a) = (OrderDual.toDual a)
@[simp]
theorem toDual_sdiff {α : Type u_2} [] (a : α) (b : α) :
OrderDual.toDual (a \ b) = OrderDual.toDual b OrderDual.toDual a
instance Prod.instCoheytingAlgebra {α : Type u_2} {β : Type u_3} [] [] :
Equations
• Prod.instCoheytingAlgebra =
instance Pi.instCoheytingAlgebra {ι : Type u_1} {α : ιType u_4} [(i : ι) → CoheytingAlgebra (α i)] :
CoheytingAlgebra ((i : ι) → α i)
Equations
• Pi.instCoheytingAlgebra =
theorem compl_le_hnot {α : Type u_2} [] {a : α} :

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

Equations
@[simp]
theorem himp_iff_imp (p : Prop) (q : Prop) :
p q pq
@[simp]
theorem compl_iff_not (p : Prop) :
@[reducible, inline]
abbrev LinearOrder.toBiheytingAlgebra {α : Type u_2} [] [] :

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 =
Instances For
instance OrderDual.instBiheytingAlgebra {α : Type u_2} [] :
Equations
• OrderDual.instBiheytingAlgebra =
instance Prod.instBiheytingAlgebra {α : Type u_2} {β : Type u_3} [] [] :
Equations
• Prod.instBiheytingAlgebra =
instance Pi.instBiheytingAlgebra {ι : Type u_1} {α : ιType u_4} [(i : ι) → BiheytingAlgebra (α i)] :
BiheytingAlgebra ((i : ι) → α i)
Equations
• Pi.instBiheytingAlgebra =
@[reducible, inline]
abbrev Function.Injective.generalizedHeytingAlgebra {α : Type u_2} {β : Type u_3} [Sup α] [Inf α] [Top α] [HImp α] (f : αβ) (hf : ) (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) :

Pullback a GeneralizedHeytingAlgebra along an injection.

Equations
Instances For
@[reducible, inline]
abbrev Function.Injective.generalizedCoheytingAlgebra {α : Type u_2} {β : Type u_3} [Sup α] [Inf α] [Bot α] [] (f : αβ) (hf : ) (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) :

Pullback a GeneralizedCoheytingAlgebra along an injection.

Equations
Instances For
@[reducible, inline]
abbrev Function.Injective.heytingAlgebra {α : Type u_2} {β : Type u_3} [Sup α] [Inf α] [Top α] [Bot α] [] [HImp α] [] (f : αβ) (hf : ) (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) :

Pullback a HeytingAlgebra along an injection.

Equations
Instances For
@[reducible, inline]
abbrev Function.Injective.coheytingAlgebra {α : Type u_2} {β : Type u_3} [Sup α] [Inf α] [Top α] [Bot α] [HNot α] [] [] (f : αβ) (hf : ) (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) :

Pullback a CoheytingAlgebra along an injection.

Equations
Instances For
@[reducible, inline]
abbrev Function.Injective.biheytingAlgebra {α : Type u_2} {β : Type u_3} [Sup α] [Inf α] [Top α] [Bot α] [] [HNot α] [HImp α] [] [] (f : αβ) (hf : ) (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) :

Pullback a BiheytingAlgebra along an injection.

Equations
Instances For
@[simp]
theorem PUnit.top_eq :
@[simp]
theorem PUnit.bot_eq :
@[simp]
@[simp]
@[simp]
theorem PUnit.compl_eq (a : PUnit.{u + 1} ) :
@[simp]
@[simp]
theorem PUnit.hnot_eq (a : PUnit.{u + 1} ) :
@[simp]