mathlib3 documentation

order.heyting.basic

Heyting algebras #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

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

Notation #

References #

Tags #

Heyting, Brouwer, algebra, implication, negation, intuitionistic

Notation #

source
@[class]
structure has_himp (α : Type u_4) :
Type u_4

Syntax typeclass for Heyting implication ⇨.

Instances of this typeclass
Instances of other typeclasses for has_himp
  • has_himp.has_sizeof_inst
source
@[class]
structure has_hnot (α : Type u_4) :
Type u_4
  • hnot : α → α

Syntax typeclass for Heyting negation ￢.

The difference between has_compl and has_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.

Instances of this typeclass
Instances of other typeclasses for has_hnot
  • has_hnot.has_sizeof_inst
source
@[protected, instance]
def prod.has_himp {α : Type u_2} {β : Type u_3} [has_himp α] [has_himp β] :
has_himp (α × β)
Equations
source
@[protected, instance]
def prod.has_hnot {α : Type u_2} {β : Type u_3} [has_hnot α] [has_hnot β] :
has_hnot (α × β)
Equations
source
@[protected, instance]
def prod.has_sdiff {α : Type u_2} {β : Type u_3} [has_sdiff α] [has_sdiff β] :
has_sdiff (α × β)
Equations
source
@[protected, instance]
def prod.has_compl {α : Type u_2} {β : Type u_3} [has_compl α] [has_compl β] :
has_compl (α × β)
Equations
source
@[simp]
theorem fst_himp {α : Type u_2} {β : Type u_3} [has_himp α] [has_himp β] (a b : α × β) :
(a ⇨ b).fst = a.fst ⇨ b.fst
source
@[simp]
theorem snd_himp {α : Type u_2} {β : Type u_3} [has_himp α] [has_himp β] (a b : α × β) :
(a ⇨ b).snd = a.snd ⇨ b.snd
source
@[simp]
theorem fst_hnot {α : Type u_2} {β : Type u_3} [has_hnot α] [has_hnot β] (a : α × β) :
(￢a).fst = ￢a.fst
source
@[simp]
theorem snd_hnot {α : Type u_2} {β : Type u_3} [has_hnot α] [has_hnot β] (a : α × β) :
(￢a).snd = ￢a.snd
source
@[simp]
theorem fst_sdiff {α : Type u_2} {β : Type u_3} [has_sdiff α] [has_sdiff β] (a b : α × β) :
(a \ b).fst = a.fst \ b.fst
source
@[simp]
theorem snd_sdiff {α : Type u_2} {β : Type u_3} [has_sdiff α] [has_sdiff β] (a b : α × β) :
(a \ b).snd = a.snd \ b.snd
source
@[simp]
theorem fst_compl {α : Type u_2} {β : Type u_3} [has_compl α] [has_compl β] (a : α × β) :
aᶜ.fst = a.fstᶜ
source
@[simp]
theorem snd_compl {α : Type u_2} {β : Type u_3} [has_compl α] [has_compl β] (a : α × β) :
aᶜ.snd = a.sndᶜ
source
@[protected, instance]
def pi.has_himp {ι : Type u_1} {π : ι → Type u_4} [Π (i : ι), has_himp (π i)] :
has_himp (Π (i : ι), π i)
Equations
source
@[protected, instance]
def pi.has_hnot {ι : Type u_1} {π : ι → Type u_4} [Π (i : ι), has_hnot (π i)] :
has_hnot (Π (i : ι), π i)
Equations
source
theorem pi.himp_def {ι : Type u_1} {π : ι → Type u_4} [Π (i : ι), has_himp (π i)] (a b : Π (i : ι), π i) :
a ⇨ b = λ (i : ι), a i ⇨ b i
source
theorem pi.hnot_def {ι : Type u_1} {π : ι → Type u_4} [Π (i : ι), has_hnot (π i)] (a : Π (i : ι), π i) :
￢a = λ (i : ι), ￢a i
source
@[simp]
theorem pi.himp_apply {ι : Type u_1} {π : ι → Type u_4} [Π (i : ι), has_himp (π i)] (a b : Π (i : ι), π i) (i : ι) :
(a ⇨ b) i = a i ⇨ b i
source
@[simp]
theorem pi.hnot_apply {ι : Type u_1} {π : ι → Type u_4} [Π (i : ι), has_hnot (π i)] (a : Π (i : ι), π i) (i : ι) :
(￢a) i = ￢a i
source
@[instance]
def generalized_heyting_algebra.to_lattice (α : Type u_4) [self : generalized_heyting_algebra α] :
lattice α
source
@[class]
structure generalized_heyting_algebra (α : Type u_4) :
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 heyting_algebra by not requiring a bottom element.

Instances of this typeclass
Instances of other typeclasses for generalized_heyting_algebra
  • generalized_heyting_algebra.has_sizeof_inst
source
@[instance]
def generalized_heyting_algebra.to_has_himp (α : Type u_4) [self : generalized_heyting_algebra α] :
has_himp α
source
@[instance]
def generalized_heyting_algebra.to_has_top (α : Type u_4) [self : generalized_heyting_algebra α] :
has_top α
source
@[instance]
def generalized_coheyting_algebra.to_has_bot (α : Type u_4) [self : generalized_coheyting_algebra α] :
has_bot α
source
@[instance]
def generalized_coheyting_algebra.to_has_sdiff (α : Type u_4) [self : generalized_coheyting_algebra α] :
has_sdiff α
source
@[instance]
def generalized_coheyting_algebra.to_lattice (α : Type u_4) [self : generalized_coheyting_algebra α] :
lattice α
source
@[class]
structure generalized_coheyting_algebra (α : Type u_4) :
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 coheyting_algebra by not requiring a top element.

Instances of this typeclass
Instances of other typeclasses for generalized_coheyting_algebra
  • generalized_coheyting_algebra.has_sizeof_inst
source
@[class]
structure heyting_algebra (α : Type u_4) :
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 ⊓.

Instances of this typeclass
Instances of other typeclasses for heyting_algebra
  • heyting_algebra.has_sizeof_inst
source
@[instance]
def heyting_algebra.to_has_compl (α : Type u_4) [self : heyting_algebra α] :
has_compl α
source
@[instance]
def heyting_algebra.to_has_bot (α : Type u_4) [self : heyting_algebra α] :
has_bot α
source
@[instance]
def heyting_algebra.to_generalized_heyting_algebra (α : Type u_4) [self : heyting_algebra α] :
generalized_heyting_algebra α
source
@[instance]
def coheyting_algebra.to_has_hnot (α : Type u_4) [self : coheyting_algebra α] :
has_hnot α
source
@[instance]
def coheyting_algebra.to_generalized_coheyting_algebra (α : Type u_4) [self : coheyting_algebra α] :
generalized_coheyting_algebra α
source
@[class]
structure coheyting_algebra (α : Type u_4) :
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.

Instances of this typeclass
Instances of other typeclasses for coheyting_algebra
  • coheyting_algebra.has_sizeof_inst
source
@[instance]
def coheyting_algebra.to_has_top (α : Type u_4) [self : coheyting_algebra α] :
has_top α
source
@[instance]
def biheyting_algebra.to_has_hnot (α : Type u_4) [self : biheyting_algebra α] :
has_hnot α
source
@[class]
structure biheyting_algebra (α : Type u_4) :
Type u_4

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

Instances of this typeclass
Instances of other typeclasses for biheyting_algebra
  • biheyting_algebra.has_sizeof_inst
source
@[instance]
def biheyting_algebra.to_heyting_algebra (α : Type u_4) [self : biheyting_algebra α] :
heyting_algebra α
source
@[instance]
def biheyting_algebra.to_has_sdiff (α : Type u_4) [self : biheyting_algebra α] :
has_sdiff α
source
@[protected, instance]
def generalized_heyting_algebra.to_order_top {α : Type u_2} [generalized_heyting_algebra α] :
order_top α
Equations
source
@[protected, instance]
def generalized_coheyting_algebra.to_order_bot {α : Type u_2} [generalized_coheyting_algebra α] :
order_bot α
Equations
source
@[protected, instance]
def heyting_algebra.to_bounded_order {α : Type u_2} [heyting_algebra α] :
bounded_order α
Equations
source
@[protected, instance]
def coheyting_algebra.to_bounded_order {α : Type u_2} [coheyting_algebra α] :
bounded_order α
Equations
source
@[protected, instance]
def biheyting_algebra.to_coheyting_algebra {α : Type u_2} [biheyting_algebra α] :
coheyting_algebra α
Equations
source
@[reducible]
def heyting_algebra.of_himp {α : Type u_2} [distrib_lattice α] [bounded_order α] (himp : α → α → α) (le_himp_iff : ∀ (a b c : α), a ≤ himp b c ↔ a ⊓ b ≤ c) :
heyting_algebra α

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

Equations
source
@[reducible]
def heyting_algebra.of_compl {α : Type u_2} [distrib_lattice α] [bounded_order α] (compl : α → α) (le_himp_iff : ∀ (a b c : α), a ≤ compl b ⊔ c ↔ a ⊓ b ≤ c) :
heyting_algebra α

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

Equations
source
@[reducible]
def coheyting_algebra.of_sdiff {α : Type u_2} [distrib_lattice α] [bounded_order α] (sdiff : α → α → α) (sdiff_le_iff : ∀ (a b c : α), sdiff a b ≤ c ↔ a ≤ b ⊔ c) :
coheyting_algebra α

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

Equations
source
@[reducible]
def coheyting_algebra.of_hnot {α : Type u_2} [distrib_lattice α] [bounded_order α] (hnot : α → α) (sdiff_le_iff : ∀ (a b c : α), a ⊓ hnot b ≤ c ↔ a ≤ b ⊔ c) :
coheyting_algebra α

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

Equations
source
@[simp]
theorem le_himp_iff {α : Type u_2} [generalized_heyting_algebra α] {a b c : α} :
a ≤ b ⇨ c ↔ a ⊓ b ≤ c
source
theorem le_himp_iff' {α : Type u_2} [generalized_heyting_algebra α] {a b c : α} :
a ≤ b ⇨ c ↔ b ⊓ a ≤ c
source
theorem le_himp_comm {α : Type u_2} [generalized_heyting_algebra α] {a b c : α} :
a ≤ b ⇨ c ↔ b ≤ a ⇨ c
source
theorem le_himp {α : Type u_2} [generalized_heyting_algebra α] {a b : α} :
a ≤ b ⇨ a
source
@[simp]
theorem le_himp_iff_left {α : Type u_2} [generalized_heyting_algebra α] {a b : α} :
a ≤ a ⇨ b ↔ a ≤ b
source
@[simp]
theorem himp_self {α : Type u_2} [generalized_heyting_algebra α] {a : α} :
a ⇨ a = ⊤
source
theorem himp_inf_le {α : Type u_2} [generalized_heyting_algebra α] {a b : α} :
(a ⇨ b) ⊓ a ≤ b
source
theorem inf_himp_le {α : Type u_2} [generalized_heyting_algebra α] {a b : α} :
a ⊓ (a ⇨ b) ≤ b
source
@[simp]
theorem inf_himp {α : Type u_2} [generalized_heyting_algebra α] (a b : α) :
a ⊓ (a ⇨ b) = a ⊓ b
source
@[simp]
theorem himp_inf_self {α : Type u_2} [generalized_heyting_algebra α] (a b : α) :
(a ⇨ b) ⊓ a = b ⊓ a
source
@[simp]
theorem himp_eq_top_iff {α : Type u_2} [generalized_heyting_algebra α] {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.

source
@[simp]
theorem himp_top {α : Type u_2} [generalized_heyting_algebra α] {a : α} :
a ⇨ ⊤ = ⊤
source
@[simp]
theorem top_himp {α : Type u_2} [generalized_heyting_algebra α] {a : α} :
⊤ ⇨ a = a
source
theorem himp_himp {α : Type u_2} [generalized_heyting_algebra α] (a b c : α) :
a ⇨ b ⇨ c = a ⊓ b ⇨ c
source
@[simp]
theorem himp_le_himp_himp_himp {α : Type u_2} [generalized_heyting_algebra α] {a b c : α} :
b ⇨ c ≤ (a ⇨ b) ⇨ a ⇨ c
source
theorem himp_left_comm {α : Type u_2} [generalized_heyting_algebra α] (a b c : α) :
a ⇨ b ⇨ c = b ⇨ a ⇨ c
source
@[simp]
theorem himp_idem {α : Type u_2} [generalized_heyting_algebra α] {a b : α} :
b ⇨ b ⇨ a = b ⇨ a
source
theorem himp_inf_distrib {α : Type u_2} [generalized_heyting_algebra α] (a b c : α) :
a ⇨ b ⊓ c = (a ⇨ b) ⊓ (a ⇨ c)
source
theorem sup_himp_distrib {α : Type u_2} [generalized_heyting_algebra α] (a b c : α) :
a ⊔ b ⇨ c = (a ⇨ c) ⊓ (b ⇨ c)
source
theorem himp_le_himp_left {α : Type u_2} [generalized_heyting_algebra α] {a b c : α} (h : a ≤ b) :
c ⇨ a ≤ c ⇨ b
source
theorem himp_le_himp_right {α : Type u_2} [generalized_heyting_algebra α] {a b c : α} (h : a ≤ b) :
b ⇨ c ≤ a ⇨ c
source
theorem himp_le_himp {α : Type u_2} [generalized_heyting_algebra α] {a b c d : α} (hab : a ≤ b) (hcd : c ≤ d) :
b ⇨ c ≤ a ⇨ d
source
@[simp]
theorem sup_himp_self_left {α : Type u_2} [generalized_heyting_algebra α] (a b : α) :
a ⊔ b ⇨ a = b ⇨ a
source
@[simp]
theorem sup_himp_self_right {α : Type u_2} [generalized_heyting_algebra α] (a b : α) :
a ⊔ b ⇨ b = a ⇨ b
source
theorem codisjoint.himp_eq_right {α : Type u_2} [generalized_heyting_algebra α] {a b : α} (h : codisjoint a b) :
b ⇨ a = a
source
theorem codisjoint.himp_eq_left {α : Type u_2} [generalized_heyting_algebra α] {a b : α} (h : codisjoint a b) :
a ⇨ b = b
source
theorem codisjoint.himp_inf_cancel_right {α : Type u_2} [generalized_heyting_algebra α] {a b : α} (h : codisjoint a b) :
a ⇨ a ⊓ b = b
source
theorem codisjoint.himp_inf_cancel_left {α : Type u_2} [generalized_heyting_algebra α] {a b : α} (h : codisjoint a b) :
b ⇨ a ⊓ b = a
source
theorem codisjoint.himp_le_of_right_le {α : Type u_2} [generalized_heyting_algebra α] {a b c : α} (hac : codisjoint a c) (hba : b ≤ a) :
c ⇨ b ≤ a

See himp_le for a stronger version in Boolean algebras.

source
theorem le_himp_himp {α : Type u_2} [generalized_heyting_algebra α] {a b : α} :
a ≤ (a ⇨ b) ⇨ b
source
theorem himp_triangle {α : Type u_2} [generalized_heyting_algebra α] (a b c : α) :
(a ⇨ b) ⊓ (b ⇨ c) ≤ a ⇨ c
source
theorem himp_inf_himp_cancel {α : Type u_2} [generalized_heyting_algebra α] {a b c : α} (hba : b ≤ a) (hcb : c ≤ b) :
(a ⇨ b) ⊓ (b ⇨ c) = a ⇨ c
source
@[protected, instance]
def generalized_heyting_algebra.to_distrib_lattice {α : Type u_2} [generalized_heyting_algebra α] :
distrib_lattice α
Equations
source
@[protected, instance]
def order_dual.generalized_coheyting_algebra {α : Type u_2} [generalized_heyting_algebra α] :
generalized_coheyting_algebra αᵒᵈ
Equations
source
@[protected, instance]
def prod.generalized_heyting_algebra {α : Type u_2} {β : Type u_3} [generalized_heyting_algebra α] [generalized_heyting_algebra β] :
generalized_heyting_algebra (α × β)
Equations
source
@[protected, instance]
def pi.generalized_heyting_algebra {ι : Type u_1} {α : ι → Type u_2} [Π (i : ι), generalized_heyting_algebra (α i)] :
generalized_heyting_algebra (Π (i : ι), α i)
Equations
source
@[simp]
theorem sdiff_le_iff {α : Type u_2} [generalized_coheyting_algebra α] {a b c : α} :
a \ b ≤ c ↔ a ≤ b ⊔ c
source
theorem sdiff_le_iff' {α : Type u_2} [generalized_coheyting_algebra α] {a b c : α} :
a \ b ≤ c ↔ a ≤ c ⊔ b
source
theorem sdiff_le_comm {α : Type u_2} [generalized_coheyting_algebra α] {a b c : α} :
a \ b ≤ c ↔ a \ c ≤ b
source
theorem sdiff_le {α : Type u_2} [generalized_coheyting_algebra α] {a b : α} :
a \ b ≤ a
source
theorem disjoint.disjoint_sdiff_left {α : Type u_2} [generalized_coheyting_algebra α] {a b c : α} (h : disjoint a b) :
disjoint (a \ c) b
source
theorem disjoint.disjoint_sdiff_right {α : Type u_2} [generalized_coheyting_algebra α] {a b c : α} (h : disjoint a b) :
disjoint a (b \ c)
source
@[simp]
theorem sdiff_le_iff_left {α : Type u_2} [generalized_coheyting_algebra α] {a b : α} :
a \ b ≤ b ↔ a ≤ b
source
@[simp]
theorem sdiff_self {α : Type u_2} [generalized_coheyting_algebra α] {a : α} :
a \ a = ⊥
source
theorem le_sup_sdiff {α : Type u_2} [generalized_coheyting_algebra α] {a b : α} :
a ≤ b ⊔ a \ b
source
theorem le_sdiff_sup {α : Type u_2} [generalized_coheyting_algebra α] {a b : α} :
a ≤ a \ b ⊔ b
source
@[simp]
theorem sup_sdiff_left {α : Type u_2} [generalized_coheyting_algebra α] {a b : α} :
a ⊔ a \ b = a
source
@[simp]
theorem sup_sdiff_right {α : Type u_2} [generalized_coheyting_algebra α] {a b : α} :
a \ b ⊔ a = a
source
@[simp]
theorem inf_sdiff_left {α : Type u_2} [generalized_coheyting_algebra α] {a b : α} :
a \ b ⊓ a = a \ b
source
@[simp]
theorem inf_sdiff_right {α : Type u_2} [generalized_coheyting_algebra α] {a b : α} :
a ⊓ a \ b = a \ b
source
@[simp]
theorem sup_sdiff_self {α : Type u_2} [generalized_coheyting_algebra α] (a b : α) :
a ⊔ b \ a = a ⊔ b
source
@[simp]
theorem sdiff_sup_self {α : Type u_2} [generalized_coheyting_algebra α] (a b : α) :
b \ a ⊔ a = b ⊔ a
source
theorem sup_sdiff_self_left {α : Type u_2} [generalized_coheyting_algebra α] (a b : α) :
b \ a ⊔ a = b ⊔ a

Alias of sdiff_sup_self.

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

Alias of sup_sdiff_self.

source
theorem sup_sdiff_eq_sup {α : Type u_2} [generalized_coheyting_algebra α] {a b c : α} (h : c ≤ a) :
a ⊔ b \ c = a ⊔ b
source
theorem sup_sdiff_cancel' {α : Type u_2} [generalized_coheyting_algebra α] {a b c : α} (hab : a ≤ b) (hbc : b ≤ c) :
b ⊔ c \ a = c
source
theorem sup_sdiff_cancel_right {α : Type u_2} [generalized_coheyting_algebra α] {a b : α} (h : a ≤ b) :
a ⊔ b \ a = b
source
theorem sdiff_sup_cancel {α : Type u_2} [generalized_coheyting_algebra α] {a b : α} (h : b ≤ a) :
a \ b ⊔ b = a
source
theorem sup_le_of_le_sdiff_left {α : Type u_2} [generalized_coheyting_algebra α] {a b c : α} (h : b ≤ c \ a) (hac : a ≤ c) :
a ⊔ b ≤ c
source
theorem sup_le_of_le_sdiff_right {α : Type u_2} [generalized_coheyting_algebra α] {a b c : α} (h : a ≤ c \ b) (hbc : b ≤ c) :
a ⊔ b ≤ c
source
@[simp]
theorem sdiff_eq_bot_iff {α : Type u_2} [generalized_coheyting_algebra α] {a b : α} :
a \ b = ⊥ ↔ a ≤ b
source
@[simp]
theorem sdiff_bot {α : Type u_2} [generalized_coheyting_algebra α] {a : α} :
a \ ⊥ = a
source
@[simp]
theorem bot_sdiff {α : Type u_2} [generalized_coheyting_algebra α] {a : α} :
⊥ \ a = ⊥
source
@[simp]
theorem sdiff_sdiff_sdiff_le_sdiff {α : Type u_2} [generalized_coheyting_algebra α] {a b c : α} :
a \ b \ (a \ c) ≤ c \ b
source
theorem sdiff_sdiff {α : Type u_2} [generalized_coheyting_algebra α] (a b c : α) :
a \ b \ c = a \ (b ⊔ c)
source
theorem sdiff_sdiff_left {α : Type u_2} [generalized_coheyting_algebra α] {a b c : α} :
a \ b \ c = a \ (b ⊔ c)
source
theorem sdiff_right_comm {α : Type u_2} [generalized_coheyting_algebra α] (a b c : α) :
a \ b \ c = a \ c \ b
source
theorem sdiff_sdiff_comm {α : Type u_2} [generalized_coheyting_algebra α] {a b c : α} :
a \ b \ c = a \ c \ b
source
@[simp]
theorem sdiff_idem {α : Type u_2} [generalized_coheyting_algebra α] {a b : α} :
a \ b \ b = a \ b
source
@[simp]
theorem sdiff_sdiff_self {α : Type u_2} [generalized_coheyting_algebra α] {a b : α} :
a \ b \ a = ⊥
source
theorem sup_sdiff_distrib {α : Type u_2} [generalized_coheyting_algebra α] (a b c : α) :
(a ⊔ b) \ c = a \ c ⊔ b \ c
source
theorem sdiff_inf_distrib {α : Type u_2} [generalized_coheyting_algebra α] (a b c : α) :
a \ (b ⊓ c) = a \ b ⊔ a \ c
source
theorem sup_sdiff {α : Type u_2} [generalized_coheyting_algebra α] {a b c : α} :
(a ⊔ b) \ c = a \ c ⊔ b \ c
source
@[simp]
theorem sup_sdiff_right_self {α : Type u_2} [generalized_coheyting_algebra α] {a b : α} :
(a ⊔ b) \ b = a \ b
source
@[simp]
theorem sup_sdiff_left_self {α : Type u_2} [generalized_coheyting_algebra α] {a b : α} :
(a ⊔ b) \ a = b \ a
source
theorem sdiff_le_sdiff_right {α : Type u_2} [generalized_coheyting_algebra α] {a b c : α} (h : a ≤ b) :
a \ c ≤ b \ c
source
theorem sdiff_le_sdiff_left {α : Type u_2} [generalized_coheyting_algebra α] {a b c : α} (h : a ≤ b) :
c \ b ≤ c \ a
source
theorem sdiff_le_sdiff {α : Type u_2} [generalized_coheyting_algebra α] {a b c d : α} (hab : a ≤ b) (hcd : c ≤ d) :
a \ d ≤ b \ c
source
theorem sdiff_inf {α : Type u_2} [generalized_coheyting_algebra α] {a b c : α} :
a \ (b ⊓ c) = a \ b ⊔ a \ c
source
@[simp]
theorem sdiff_inf_self_left {α : Type u_2} [generalized_coheyting_algebra α] (a b : α) :
a \ (a ⊓ b) = a \ b
source
@[simp]
theorem sdiff_inf_self_right {α : Type u_2} [generalized_coheyting_algebra α] (a b : α) :
b \ (a ⊓ b) = b \ a
source
theorem disjoint.sdiff_eq_left {α : Type u_2} [generalized_coheyting_algebra α] {a b : α} (h : disjoint a b) :
a \ b = a
source
theorem disjoint.sdiff_eq_right {α : Type u_2} [generalized_coheyting_algebra α] {a b : α} (h : disjoint a b) :
b \ a = b
source
theorem disjoint.sup_sdiff_cancel_left {α : Type u_2} [generalized_coheyting_algebra α] {a b : α} (h : disjoint a b) :
(a ⊔ b) \ a = b
source
theorem disjoint.sup_sdiff_cancel_right {α : Type u_2} [generalized_coheyting_algebra α] {a b : α} (h : disjoint a b) :
(a ⊔ b) \ b = a
source
theorem disjoint.le_sdiff_of_le_left {α : Type u_2} [generalized_coheyting_algebra α] {a b c : α} (hac : disjoint a c) (hab : a ≤ b) :
a ≤ b \ c

See le_sdiff for a stronger version in generalised Boolean algebras.

source
theorem sdiff_sdiff_le {α : Type u_2} [generalized_coheyting_algebra α] {a b : α} :
a \ (a \ b) ≤ b
source
theorem sdiff_triangle {α : Type u_2} [generalized_coheyting_algebra α] (a b c : α) :
a \ c ≤ a \ b ⊔ b \ c
source
theorem sdiff_sup_sdiff_cancel {α : Type u_2} [generalized_coheyting_algebra α] {a b c : α} (hba : b ≤ a) (hcb : c ≤ b) :
a \ b ⊔ b \ c = a \ c
source
theorem sdiff_le_sdiff_of_sup_le_sup_left {α : Type u_2} [generalized_coheyting_algebra α] {a b c : α} (h : c ⊔ a ≤ c ⊔ b) :
a \ c ≤ b \ c
source
theorem sdiff_le_sdiff_of_sup_le_sup_right {α : Type u_2} [generalized_coheyting_algebra α] {a b c : α} (h : a ⊔ c ≤ b ⊔ c) :
a \ c ≤ b \ c
source
@[simp]
theorem inf_sdiff_sup_left {α : Type u_2} [generalized_coheyting_algebra α] {a b c : α} :
a \ c ⊓ (a ⊔ b) = a \ c
source
@[simp]
theorem inf_sdiff_sup_right {α : Type u_2} [generalized_coheyting_algebra α] {a b c : α} :
a \ c ⊓ (b ⊔ a) = a \ c
source
@[protected, instance]
def generalized_coheyting_algebra.to_distrib_lattice {α : Type u_2} [generalized_coheyting_algebra α] :
distrib_lattice α
Equations
source
@[protected, instance]
def order_dual.generalized_heyting_algebra {α : Type u_2} [generalized_coheyting_algebra α] :
generalized_heyting_algebra αᵒᵈ
Equations
source
@[protected, instance]
def prod.generalized_coheyting_algebra {α : Type u_2} {β : Type u_3} [generalized_coheyting_algebra α] [generalized_coheyting_algebra β] :
generalized_coheyting_algebra (α × β)
Equations
source
@[protected, instance]
def pi.generalized_coheyting_algebra {ι : Type u_1} {α : ι → Type u_2} [Π (i : ι), generalized_coheyting_algebra (α i)] :
generalized_coheyting_algebra (Π (i : ι), α i)
Equations
source
@[simp]
theorem himp_bot {α : Type u_2} [heyting_algebra α] (a : α) :
a ⇨ ⊥ = aᶜ
source
@[simp]
theorem bot_himp {α : Type u_2} [heyting_algebra α] (a : α) :
⊥ ⇨ a = ⊤
source
theorem compl_sup_distrib {α : Type u_2} [heyting_algebra α] (a b : α) :
(a ⊔ b)ᶜ = aᶜ ⊓ bᶜ
source
@[simp]
theorem compl_sup {α : Type u_2} [heyting_algebra α] {a b : α} :
(a ⊔ b)ᶜ = aᶜ ⊓ bᶜ
source
theorem compl_le_himp {α : Type u_2} [heyting_algebra α] {a b : α} :
aᶜ ≤ a ⇨ b
source
theorem compl_sup_le_himp {α : Type u_2} [heyting_algebra α] {a b : α} :
aᶜ ⊔ b ≤ a ⇨ b
source
theorem sup_compl_le_himp {α : Type u_2} [heyting_algebra α] {a b : α} :
b ⊔ aᶜ ≤ a ⇨ b
source
@[simp]
theorem himp_compl {α : Type u_2} [heyting_algebra α] (a : α) :
a ⇨ aᶜ = aᶜ
source
theorem himp_compl_comm {α : Type u_2} [heyting_algebra α] (a b : α) :
a ⇨ bᶜ = b ⇨ aᶜ
source
theorem le_compl_iff_disjoint_right {α : Type u_2} [heyting_algebra α] {a b : α} :
a ≤ bᶜ ↔ disjoint a b
source
theorem le_compl_iff_disjoint_left {α : Type u_2} [heyting_algebra α] {a b : α} :
a ≤ bᶜ ↔ disjoint b a
source
theorem le_compl_comm {α : Type u_2} [heyting_algebra α] {a b : α} :
a ≤ bᶜ ↔ b ≤ aᶜ
source
theorem disjoint.le_compl_right {α : Type u_2} [heyting_algebra α] {a b : α} :
disjoint a b → a ≤ bᶜ

Alias of the reverse direction of le_compl_iff_disjoint_right.

source
theorem disjoint.le_compl_left {α : Type u_2} [heyting_algebra α] {a b : α} :
disjoint b a → a ≤ bᶜ

Alias of the reverse direction of le_compl_iff_disjoint_left.

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

Alias of le_compl_comm.

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

Alias of the forward direction of le_compl_comm.

source
theorem disjoint_compl_left {α : Type u_2} [heyting_algebra α] {a : α} :
disjoint aᶜ a
source
theorem disjoint_compl_right {α : Type u_2} [heyting_algebra α] {a : α} :
disjoint a aᶜ
source
theorem has_le.le.disjoint_compl_left {α : Type u_2} [heyting_algebra α] {a b : α} (h : b ≤ a) :
disjoint aᶜ b
source
theorem has_le.le.disjoint_compl_right {α : Type u_2} [heyting_algebra α] {a b : α} (h : a ≤ b) :
disjoint a bᶜ
source
theorem is_compl.compl_eq {α : Type u_2} [heyting_algebra α] {a b : α} (h : is_compl a b) :
aᶜ = b
source
theorem is_compl.eq_compl {α : Type u_2} [heyting_algebra α] {a b : α} (h : is_compl a b) :
a = bᶜ
source
theorem compl_unique {α : Type u_2} [heyting_algebra α] {a b : α} (h₀ : a ⊓ b = ⊥) (h₁ : a ⊔ b = ⊤) :
aᶜ = b
source
@[simp]
theorem inf_compl_self {α : Type u_2} [heyting_algebra α] (a : α) :
a ⊓ aᶜ = ⊥
source
@[simp]
theorem compl_inf_self {α : Type u_2} [heyting_algebra α] (a : α) :
aᶜ ⊓ a = ⊥
source
theorem inf_compl_eq_bot {α : Type u_2} [heyting_algebra α] {a : α} :
a ⊓ aᶜ = ⊥
source
theorem compl_inf_eq_bot {α : Type u_2} [heyting_algebra α] {a : α} :
aᶜ ⊓ a = ⊥
source
@[simp]
theorem compl_top {α : Type u_2} [heyting_algebra α] :
⊤ᶜ = ⊥
source
@[simp]
theorem compl_bot {α : Type u_2} [heyting_algebra α] :
⊥ᶜ = ⊤
source
theorem le_compl_compl {α : Type u_2} [heyting_algebra α] {a : α} :
a ≤ aᶜᶜ
source
theorem compl_anti {α : Type u_2} [heyting_algebra α] :
antitone has_compl.compl
source
theorem compl_le_compl {α : Type u_2} [heyting_algebra α] {a b : α} (h : a ≤ b) :
bᶜ ≤ aᶜ
source
@[simp]
theorem compl_compl_compl {α : Type u_2} [heyting_algebra α] (a : α) :
aᶜᶜᶜ = aᶜ
source
@[simp]
theorem disjoint_compl_compl_left_iff {α : Type u_2} [heyting_algebra α] {a b : α} :
disjoint aᶜᶜ b ↔ disjoint a b
source
@[simp]
theorem disjoint_compl_compl_right_iff {α : Type u_2} [heyting_algebra α] {a b : α} :
disjoint a bᶜᶜ ↔ disjoint a b
source
theorem compl_sup_compl_le {α : Type u_2} [heyting_algebra α] {a b : α} :
aᶜ ⊔ bᶜ ≤ (a ⊓ b)ᶜ
source
theorem compl_compl_inf_distrib {α : Type u_2} [heyting_algebra α] (a b : α) :
(a ⊓ b)ᶜᶜ = aᶜᶜ ⊓ bᶜᶜ
source
theorem compl_compl_himp_distrib {α : Type u_2} [heyting_algebra α] (a b : α) :
(a ⇨ b)ᶜᶜ = aᶜᶜ ⇨ bᶜᶜ
source
@[protected, instance]
def order_dual.coheyting_algebra {α : Type u_2} [heyting_algebra α] :
coheyting_algebra αᵒᵈ
Equations
source
@[simp]
theorem of_dual_hnot {α : Type u_2} [heyting_algebra α] (a : αᵒᵈ) :
⇑order_dual.of_dual (￢a) = (⇑order_dual.of_dual a)ᶜ
source
@[simp]
theorem to_dual_compl {α : Type u_2} [heyting_algebra α] (a : α) :
⇑order_dual.to_dual aᶜ = ￢⇑order_dual.to_dual a
source
@[protected, instance]
def prod.heyting_algebra {α : Type u_2} {β : Type u_3} [heyting_algebra α] [heyting_algebra β] :
heyting_algebra (α × β)
Equations
source
@[protected, instance]
def pi.heyting_algebra {ι : Type u_1} {α : ι → Type u_2} [Π (i : ι), heyting_algebra (α i)] :
heyting_algebra (Π (i : ι), α i)
Equations
source
@[simp]
theorem top_sdiff' {α : Type u_2} [coheyting_algebra α] (a : α) :
⊤ \ a = ￢a
source
@[simp]
theorem sdiff_top {α : Type u_2} [coheyting_algebra α] (a : α) :
a \ ⊤ = ⊥
source
theorem hnot_inf_distrib {α : Type u_2} [coheyting_algebra α] (a b : α) :
￢(a ⊓ b) = ￢a ⊔ ￢b
source
theorem sdiff_le_hnot {α : Type u_2} [coheyting_algebra α] {a b : α} :
a \ b ≤ ￢b
source
theorem sdiff_le_inf_hnot {α : Type u_2} [coheyting_algebra α] {a b : α} :
a \ b ≤ a ⊓ ￢b
source
@[protected, instance]
def coheyting_algebra.to_distrib_lattice {α : Type u_2} [coheyting_algebra α] :
distrib_lattice α
Equations
source
@[simp]
theorem hnot_sdiff {α : Type u_2} [coheyting_algebra α] (a : α) :
￢a \ a = ￢a
source
theorem hnot_sdiff_comm {α : Type u_2} [coheyting_algebra α] (a b : α) :
￢a \ b = ￢b \ a
source
theorem hnot_le_iff_codisjoint_right {α : Type u_2} [coheyting_algebra α] {a b : α} :
￢a ≤ b ↔ codisjoint a b
source
theorem hnot_le_iff_codisjoint_left {α : Type u_2} [coheyting_algebra α] {a b : α} :
￢a ≤ b ↔ codisjoint b a
source
theorem hnot_le_comm {α : Type u_2} [coheyting_algebra α] {a b : α} :
￢a ≤ b ↔ ￢b ≤ a
source
theorem codisjoint.hnot_le_right {α : Type u_2} [coheyting_algebra α] {a b : α} :
codisjoint a b → ￢a ≤ b

Alias of the reverse direction of hnot_le_iff_codisjoint_right.

source
theorem codisjoint.hnot_le_left {α : Type u_2} [coheyting_algebra α] {a b : α} :
codisjoint b a → ￢a ≤ b

Alias of the reverse direction of hnot_le_iff_codisjoint_left.

source
theorem codisjoint_hnot_right {α : Type u_2} [coheyting_algebra α] {a : α} :
codisjoint a (￢a)
source
theorem codisjoint_hnot_left {α : Type u_2} [coheyting_algebra α] {a : α} :
codisjoint (￢a) a
source
theorem has_le.le.codisjoint_hnot_left {α : Type u_2} [coheyting_algebra α] {a b : α} (h : a ≤ b) :
codisjoint (￢a) b
source
theorem has_le.le.codisjoint_hnot_right {α : Type u_2} [coheyting_algebra α] {a b : α} (h : b ≤ a) :
codisjoint a (￢b)
source
theorem is_compl.hnot_eq {α : Type u_2} [coheyting_algebra α] {a b : α} (h : is_compl a b) :
￢a = b
source
theorem is_compl.eq_hnot {α : Type u_2} [coheyting_algebra α] {a b : α} (h : is_compl a b) :
a = ￢b
source
@[simp]
theorem sup_hnot_self {α : Type u_2} [coheyting_algebra α] (a : α) :
a ⊔ ￢a = ⊤
source
@[simp]
theorem hnot_sup_self {α : Type u_2} [coheyting_algebra α] (a : α) :
￢a ⊔ a = ⊤
source
@[simp]
theorem hnot_bot {α : Type u_2} [coheyting_algebra α] :
￢⊥ = ⊤
source
@[simp]
theorem hnot_top {α : Type u_2} [coheyting_algebra α] :
￢⊤ = ⊥
source
theorem hnot_hnot_le {α : Type u_2} [coheyting_algebra α] {a : α} :
￢￢a ≤ a
source
theorem hnot_anti {α : Type u_2} [coheyting_algebra α] :
antitone has_hnot.hnot
source
theorem hnot_le_hnot {α : Type u_2} [coheyting_algebra α] {a b : α} (h : a ≤ b) :
￢b ≤ ￢a
source
@[simp]
theorem hnot_hnot_hnot {α : Type u_2} [coheyting_algebra α] (a : α) :
￢￢￢a = ￢a
source
@[simp]
theorem codisjoint_hnot_hnot_left_iff {α : Type u_2} [coheyting_algebra α] {a b : α} :
codisjoint (￢￢a) b ↔ codisjoint a b
source
@[simp]
theorem codisjoint_hnot_hnot_right_iff {α : Type u_2} [coheyting_algebra α] {a b : α} :
codisjoint a (￢￢b) ↔ codisjoint a b
source
theorem le_hnot_inf_hnot {α : Type u_2} [coheyting_algebra α] {a b : α} :
￢(a ⊔ b) ≤ ￢a ⊓ ￢b
source
theorem hnot_hnot_sup_distrib {α : Type u_2} [coheyting_algebra α] (a b : α) :
￢￢(a ⊔ b) = ￢￢a ⊔ ￢￢b
source
theorem hnot_hnot_sdiff_distrib {α : Type u_2} [coheyting_algebra α] (a b : α) :
￢￢(a \ b) = ￢￢a \ ￢￢b
source
@[protected, instance]
def order_dual.heyting_algebra {α : Type u_2} [coheyting_algebra α] :
heyting_algebra αᵒᵈ
Equations
source
@[simp]
theorem of_dual_compl {α : Type u_2} [coheyting_algebra α] (a : αᵒᵈ) :
⇑order_dual.of_dual aᶜ = ￢⇑order_dual.of_dual a
source
@[simp]
theorem of_dual_himp {α : Type u_2} [coheyting_algebra α] (a b : αᵒᵈ) :
⇑order_dual.of_dual (a ⇨ b) = ⇑order_dual.of_dual b \ ⇑order_dual.of_dual a
source
@[simp]
theorem to_dual_hnot {α : Type u_2} [coheyting_algebra α] (a : α) :
⇑order_dual.to_dual (￢a) = (⇑order_dual.to_dual a)ᶜ
source
@[simp]
theorem to_dual_sdiff {α : Type u_2} [coheyting_algebra α] (a b : α) :
⇑order_dual.to_dual (a \ b) = ⇑order_dual.to_dual b ⇨ ⇑order_dual.to_dual a
source
@[protected, instance]
def prod.coheyting_algebra {α : Type u_2} {β : Type u_3} [coheyting_algebra α] [coheyting_algebra β] :
coheyting_algebra (α × β)
Equations
source
@[protected, instance]
def pi.coheyting_algebra {ι : Type u_1} {α : ι → Type u_2} [Π (i : ι), coheyting_algebra (α i)] :
coheyting_algebra (Π (i : ι), α i)
Equations
source
theorem compl_le_hnot {α : Type u_2} [biheyting_algebra α] {a : α} :
aᶜ ≤ ￢a
source
@[protected, instance]
def Prop.heyting_algebra  :
heyting_algebra Prop

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

Equations
source
@[simp]
theorem himp_iff_imp (p q : Prop) :
p ⇨ q ↔ p → q
source
@[simp]
theorem compl_iff_not (p : Prop) :
pᶜ ↔ ¬p
source
@[reducible]
def linear_order.to_biheyting_algebra {α : Type u_2} [linear_order α] [bounded_order α] :
biheyting_algebra α

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
source
@[protected, reducible]
def function.injective.generalized_heyting_algebra {α : Type u_2} {β : Type u_3} [has_sup α] [has_inf α] [has_top α] [has_himp α] [generalized_heyting_algebra β] (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) :
generalized_heyting_algebra α

Pullback a generalized_heyting_algebra along an injection.

Equations
source
@[protected, reducible]
def function.injective.generalized_coheyting_algebra {α : Type u_2} {β : Type u_3} [has_sup α] [has_inf α] [has_bot α] [has_sdiff α] [generalized_coheyting_algebra β] (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) :
generalized_coheyting_algebra α

Pullback a generalized_coheyting_algebra along an injection.

Equations
source
@[protected, reducible]
def function.injective.heyting_algebra {α : Type u_2} {β : Type u_3} [has_sup α] [has_inf α] [has_top α] [has_bot α] [has_compl α] [has_himp α] [heyting_algebra β] (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) :
heyting_algebra α

Pullback a heyting_algebra along an injection.

Equations
source
@[protected, reducible]
def function.injective.coheyting_algebra {α : Type u_2} {β : Type u_3} [has_sup α] [has_inf α] [has_top α] [has_bot α] [has_hnot α] [has_sdiff α] [coheyting_algebra β] (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) :
coheyting_algebra α

Pullback a coheyting_algebra along an injection.

Equations
source
@[protected, reducible]
def function.injective.biheyting_algebra {α : Type u_2} {β : Type u_3} [has_sup α] [has_inf α] [has_top α] [has_bot α] [has_compl α] [has_hnot α] [has_himp α] [has_sdiff α] [biheyting_algebra β] (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) :
biheyting_algebra α

Pullback a biheyting_algebra along an injection.

Equations
source
@[protected, instance]
def punit.biheyting_algebra  :
biheyting_algebra punit
Equations
source
@[simp]
theorem punit.top_eq  :
⊤ = punit.star
source
@[simp]
theorem punit.bot_eq  :
⊥ = punit.star
source
@[simp]
theorem punit.sup_eq (a b : punit) :
a ⊔ b = punit.star
source
@[simp]
theorem punit.inf_eq (a b : punit) :
a ⊓ b = punit.star
source
@[simp]
theorem punit.compl_eq (a : punit) :
aᶜ = punit.star
source
@[simp]
theorem punit.sdiff_eq (a b : punit) :
a \ b = punit.star
source
@[simp, nolint]
theorem punit.hnot_eq (a : punit) :
￢a = punit.star
source
@[simp]
theorem punit.himp_eq (a b : punit) :
a ⇨ b = punit.star