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 #

@[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
@[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
@[protected, instance]
def prod.has_himp {α : Type u_2} {β : Type u_3} [has_himp α] [has_himp β] :
has_himp × β)
Equations
@[protected, instance]
def prod.has_hnot {α : Type u_2} {β : Type u_3} [has_hnot α] [has_hnot β] :
has_hnot × β)
Equations
@[protected, instance]
def prod.has_sdiff {α : Type u_2} {β : Type u_3} [has_sdiff α] [has_sdiff β] :
has_sdiff × β)
Equations
@[protected, instance]
def prod.has_compl {α : Type u_2} {β : Type u_3} [has_compl α] [has_compl β] :
has_compl × β)
Equations
@[simp]
theorem fst_himp {α : Type u_2} {β : Type u_3} [has_himp α] [has_himp β] (a b : α × β) :
(a b).fst = a.fst b.fst
@[simp]
theorem snd_himp {α : Type u_2} {β : Type u_3} [has_himp α] [has_himp β] (a b : α × β) :
(a b).snd = a.snd b.snd
@[simp]
theorem fst_hnot {α : Type u_2} {β : Type u_3} [has_hnot α] [has_hnot β] (a : α × β) :
@[simp]
theorem snd_hnot {α : Type u_2} {β : Type u_3} [has_hnot α] [has_hnot β] (a : α × β) :
@[simp]
theorem fst_sdiff {α : Type u_2} {β : Type u_3} [has_sdiff α] [has_sdiff β] (a b : α × β) :
(a \ b).fst = a.fst \ b.fst
@[simp]
theorem snd_sdiff {α : Type u_2} {β : Type u_3} [has_sdiff α] [has_sdiff β] (a b : α × β) :
(a \ b).snd = a.snd \ b.snd
@[simp]
theorem fst_compl {α : Type u_2} {β : Type u_3} [has_compl α] [has_compl β] (a : α × β) :
@[simp]
theorem snd_compl {α : Type u_2} {β : Type u_3} [has_compl α] [has_compl β] (a : α × β) :
@[protected, instance]
def pi.has_himp {ι : Type u_1} {π : ι Type u_4} [Π (i : ι), has_himp (π i)] :
has_himp (Π (i : ι), π i)
Equations
@[protected, instance]
def pi.has_hnot {ι : Type u_1} {π : ι Type u_4} [Π (i : ι), has_hnot (π i)] :
has_hnot (Π (i : ι), π i)
Equations
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
theorem pi.hnot_def {ι : Type u_1} {π : ι Type u_4} [Π (i : ι), has_hnot (π i)] (a : Π (i : ι), π i) :
a = λ (i : ι), a i
@[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
@[simp]
theorem pi.hnot_apply {ι : Type u_1} {π : ι Type u_4} [Π (i : ι), has_hnot (π i)] (a : Π (i : ι), π i) (i : ι) :
(a) i = a i
@[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
@[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
@[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
@[instance]
def heyting_algebra.to_has_compl (α : Type u_4) [self : heyting_algebra α] :
@[instance]
def heyting_algebra.to_has_bot (α : Type u_4) [self : heyting_algebra α] :
@[instance]
@[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
@[instance]
def coheyting_algebra.to_has_top (α : Type u_4) [self : coheyting_algebra α] :
@[instance]
@[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
@[instance]
@[protected, instance]
Equations
@[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) :

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

Equations
@[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) :

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

Equations
@[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) :

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

Equations
@[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) :

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

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

@[simp]
theorem himp_top {α : Type u_2} [generalized_heyting_algebra α] {a : α} :
@[simp]
theorem top_himp {α : Type u_2} [generalized_heyting_algebra α] {a : α} :
a = a
theorem himp_himp {α : Type u_2} [generalized_heyting_algebra α] (a b c : α) :
a b c = a b c
@[simp]
theorem himp_le_himp_himp_himp {α : Type u_2} [generalized_heyting_algebra α] {a b c : α} :
b c (a b) a c
theorem himp_left_comm {α : Type u_2} [generalized_heyting_algebra α] (a b c : α) :
a b c = b a c
@[simp]
theorem himp_idem {α : Type u_2} [generalized_heyting_algebra α] {a b : α} :
b b a = b a
theorem himp_inf_distrib {α : Type u_2} [generalized_heyting_algebra α] (a b c : α) :
a b c = (a b) (a c)
theorem sup_himp_distrib {α : Type u_2} [generalized_heyting_algebra α] (a b c : α) :
a b c = (a c) (b c)
theorem himp_le_himp_left {α : Type u_2} [generalized_heyting_algebra α] {a b c : α} (h : a b) :
c a c b
theorem himp_le_himp_right {α : Type u_2} [generalized_heyting_algebra α] {a b c : α} (h : a b) :
b c a c
theorem himp_le_himp {α : Type u_2} [generalized_heyting_algebra α] {a b c d : α} (hab : a b) (hcd : c d) :
b c a d
@[simp]
theorem sup_himp_self_left {α : Type u_2} [generalized_heyting_algebra α] (a b : α) :
a b a = b a
@[simp]
theorem sup_himp_self_right {α : Type u_2} [generalized_heyting_algebra α] (a b : α) :
a b b = a b
theorem codisjoint.himp_eq_right {α : Type u_2} [generalized_heyting_algebra α] {a b : α} (h : codisjoint a b) :
b a = a
theorem codisjoint.himp_eq_left {α : Type u_2} [generalized_heyting_algebra α] {a b : α} (h : codisjoint a b) :
a b = b
theorem codisjoint.himp_inf_cancel_right {α : Type u_2} [generalized_heyting_algebra α] {a b : α} (h : codisjoint a b) :
a a b = b
theorem codisjoint.himp_inf_cancel_left {α : Type u_2} [generalized_heyting_algebra α] {a b : α} (h : codisjoint a b) :
b a b = a
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.

theorem le_himp_himp {α : Type u_2} [generalized_heyting_algebra α] {a b : α} :
a (a b) b
theorem himp_triangle {α : Type u_2} [generalized_heyting_algebra α] (a b c : α) :
(a b) (b c) a c
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
@[protected, instance]
Equations
@[protected, instance]
def pi.generalized_heyting_algebra {ι : Type u_1} {α : ι Type u_2} [Π (i : ι), generalized_heyting_algebra (α i)] :
Equations
@[simp]
theorem sdiff_le_iff {α : Type u_2} [generalized_coheyting_algebra α] {a b c : α} :
a \ b c a b c
theorem sdiff_le_iff' {α : Type u_2} [generalized_coheyting_algebra α] {a b c : α} :
a \ b c a c b
theorem sdiff_le_comm {α : Type u_2} [generalized_coheyting_algebra α] {a b c : α} :
a \ b c a \ c b
theorem sdiff_le {α : Type u_2} [generalized_coheyting_algebra α] {a b : α} :
a \ b a
theorem disjoint.disjoint_sdiff_left {α : Type u_2} [generalized_coheyting_algebra α] {a b c : α} (h : disjoint a b) :
disjoint (a \ c) b
theorem disjoint.disjoint_sdiff_right {α : Type u_2} [generalized_coheyting_algebra α] {a b c : α} (h : disjoint a b) :
disjoint a (b \ c)
@[simp]
theorem sdiff_le_iff_left {α : Type u_2} [generalized_coheyting_algebra α] {a b : α} :
a \ b b a b
@[simp]
theorem sdiff_self {α : Type u_2} [generalized_coheyting_algebra α] {a : α} :
a \ a =
theorem le_sup_sdiff {α : Type u_2} [generalized_coheyting_algebra α] {a b : α} :
a b a \ b
theorem le_sdiff_sup {α : Type u_2} [generalized_coheyting_algebra α] {a b : α} :
a a \ b b
@[simp]
theorem sup_sdiff_left {α : Type u_2} [generalized_coheyting_algebra α] {a b : α} :
a a \ b = a
@[simp]
theorem sup_sdiff_right {α : Type u_2} [generalized_coheyting_algebra α] {a b : α} :
a \ b a = a
@[simp]
theorem inf_sdiff_left {α : Type u_2} [generalized_coheyting_algebra α] {a b : α} :
a \ b a = a \ b
@[simp]
theorem inf_sdiff_right {α : Type u_2} [generalized_coheyting_algebra α] {a b : α} :
a a \ b = a \ b
@[simp]
theorem sup_sdiff_self {α : Type u_2} [generalized_coheyting_algebra α] (a b : α) :
a b \ a = a b
@[simp]
theorem sdiff_sup_self {α : Type u_2} [generalized_coheyting_algebra α] (a b : α) :
b \ a a = b a
theorem sup_sdiff_self_left {α : Type u_2} [generalized_coheyting_algebra α] (a b : α) :
b \ a a = b a

Alias of sdiff_sup_self.

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

Alias of sup_sdiff_self.

theorem sup_sdiff_eq_sup {α : Type u_2} [generalized_coheyting_algebra α] {a b c : α} (h : c a) :
a b \ c = a b
theorem sup_sdiff_cancel' {α : Type u_2} [generalized_coheyting_algebra α] {a b c : α} (hab : a b) (hbc : b c) :
b c \ a = c
theorem sup_sdiff_cancel_right {α : Type u_2} [generalized_coheyting_algebra α] {a b : α} (h : a b) :
a b \ a = b
theorem sdiff_sup_cancel {α : Type u_2} [generalized_coheyting_algebra α] {a b : α} (h : b a) :
a \ b b = a
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
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
@[simp]
theorem sdiff_eq_bot_iff {α : Type u_2} [generalized_coheyting_algebra α] {a b : α} :
a \ b = a b
@[simp]
theorem sdiff_bot {α : Type u_2} [generalized_coheyting_algebra α] {a : α} :
a \ = a
@[simp]
theorem bot_sdiff {α : Type u_2} [generalized_coheyting_algebra α] {a : α} :
@[simp]
theorem sdiff_sdiff_sdiff_le_sdiff {α : Type u_2} [generalized_coheyting_algebra α] {a b c : α} :
a \ b \ (a \ c) c \ b
theorem sdiff_sdiff {α : Type u_2} [generalized_coheyting_algebra α] (a b c : α) :
a \ b \ c = a \ (b c)
theorem sdiff_sdiff_left {α : Type u_2} [generalized_coheyting_algebra α] {a b c : α} :
a \ b \ c = a \ (b c)
theorem sdiff_right_comm {α : Type u_2} [generalized_coheyting_algebra α] (a b c : α) :
a \ b \ c = a \ c \ b
theorem sdiff_sdiff_comm {α : Type u_2} [generalized_coheyting_algebra α] {a b c : α} :
a \ b \ c = a \ c \ b
@[simp]
theorem sdiff_idem {α : Type u_2} [generalized_coheyting_algebra α] {a b : α} :
a \ b \ b = a \ b
@[simp]
theorem sdiff_sdiff_self {α : Type u_2} [generalized_coheyting_algebra α] {a b : α} :
a \ b \ a =
theorem sup_sdiff_distrib {α : Type u_2} [generalized_coheyting_algebra α] (a b c : α) :
(a b) \ c = a \ c b \ c
theorem sdiff_inf_distrib {α : Type u_2} [generalized_coheyting_algebra α] (a b c : α) :
a \ (b c) = a \ b a \ c
theorem sup_sdiff {α : Type u_2} [generalized_coheyting_algebra α] {a b c : α} :
(a b) \ c = a \ c b \ c
@[simp]
theorem sup_sdiff_right_self {α : Type u_2} [generalized_coheyting_algebra α] {a b : α} :
(a b) \ b = a \ b
@[simp]
theorem sup_sdiff_left_self {α : Type u_2} [generalized_coheyting_algebra α] {a b : α} :
(a b) \ a = b \ a
theorem sdiff_le_sdiff_right {α : Type u_2} [generalized_coheyting_algebra α] {a b c : α} (h : a b) :
a \ c b \ c
theorem sdiff_le_sdiff_left {α : Type u_2} [generalized_coheyting_algebra α] {a b c : α} (h : a b) :
c \ b c \ a
theorem sdiff_le_sdiff {α : Type u_2} [generalized_coheyting_algebra α] {a b c d : α} (hab : a b) (hcd : c d) :
a \ d b \ c
theorem sdiff_inf {α : Type u_2} [generalized_coheyting_algebra α] {a b c : α} :
a \ (b c) = a \ b a \ c
@[simp]
theorem sdiff_inf_self_left {α : Type u_2} [generalized_coheyting_algebra α] (a b : α) :
a \ (a b) = a \ b
@[simp]
theorem sdiff_inf_self_right {α : Type u_2} [generalized_coheyting_algebra α] (a b : α) :
b \ (a b) = b \ a
theorem disjoint.sdiff_eq_left {α : Type u_2} [generalized_coheyting_algebra α] {a b : α} (h : disjoint a b) :
a \ b = a
theorem disjoint.sdiff_eq_right {α : Type u_2} [generalized_coheyting_algebra α] {a b : α} (h : disjoint a b) :
b \ a = b
theorem disjoint.sup_sdiff_cancel_left {α : Type u_2} [generalized_coheyting_algebra α] {a b : α} (h : disjoint a b) :
(a b) \ a = b
theorem disjoint.sup_sdiff_cancel_right {α : Type u_2} [generalized_coheyting_algebra α] {a b : α} (h : disjoint a b) :
(a b) \ b = a
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.

theorem sdiff_sdiff_le {α : Type u_2} [generalized_coheyting_algebra α] {a b : α} :
a \ (a \ b) b
theorem sdiff_triangle {α : Type u_2} [generalized_coheyting_algebra α] (a b c : α) :
a \ c a \ b b \ c
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
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
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
@[simp]
theorem inf_sdiff_sup_left {α : Type u_2} [generalized_coheyting_algebra α] {a b c : α} :
a \ c (a b) = a \ c
@[simp]
theorem inf_sdiff_sup_right {α : Type u_2} [generalized_coheyting_algebra α] {a b c : α} :
a \ c (b a) = a \ c
@[protected, instance]
def pi.generalized_coheyting_algebra {ι : Type u_1} {α : ι Type u_2} [Π (i : ι), generalized_coheyting_algebra (α i)] :
Equations
@[simp]
theorem himp_bot {α : Type u_2} [heyting_algebra α] (a : α) :
@[simp]
theorem bot_himp {α : Type u_2} [heyting_algebra α] (a : α) :
theorem compl_sup_distrib {α : Type u_2} [heyting_algebra α] (a b : α) :
(a b) = a b
@[simp]
theorem compl_sup {α : Type u_2} [heyting_algebra α] {a b : α} :
(a b) = a b
theorem compl_le_himp {α : Type u_2} [heyting_algebra α] {a b : α} :
a a b
theorem compl_sup_le_himp {α : Type u_2} [heyting_algebra α] {a b : α} :
a b a b
theorem sup_compl_le_himp {α : Type u_2} [heyting_algebra α] {a b : α} :
b a a b
@[simp]
theorem himp_compl {α : Type u_2} [heyting_algebra α] (a : α) :
a a = a
theorem himp_compl_comm {α : Type u_2} [heyting_algebra α] (a b : α) :
a b = b a
theorem le_compl_iff_disjoint_right {α : Type u_2} [heyting_algebra α] {a b : α} :
theorem le_compl_iff_disjoint_left {α : Type u_2} [heyting_algebra α] {a b : α} :
theorem le_compl_comm {α : Type u_2} [heyting_algebra α] {a b : α} :
a b b a
theorem disjoint.le_compl_right {α : Type u_2} [heyting_algebra α] {a b : α} :

Alias of the reverse direction of le_compl_iff_disjoint_right.

theorem disjoint.le_compl_left {α : Type u_2} [heyting_algebra α] {a b : α} :

Alias of the reverse direction of le_compl_iff_disjoint_left.

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

Alias of le_compl_comm.

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.

theorem disjoint_compl_left {α : Type u_2} [heyting_algebra α] {a : α} :
theorem disjoint_compl_right {α : Type u_2} [heyting_algebra α] {a : α} :
theorem has_le.le.disjoint_compl_left {α : Type u_2} [heyting_algebra α] {a b : α} (h : b a) :
theorem has_le.le.disjoint_compl_right {α : Type u_2} [heyting_algebra α] {a b : α} (h : a b) :
theorem is_compl.compl_eq {α : Type u_2} [heyting_algebra α] {a b : α} (h : is_compl a b) :
a = b
theorem is_compl.eq_compl {α : Type u_2} [heyting_algebra α] {a b : α} (h : is_compl a b) :
a = b
theorem compl_unique {α : Type u_2} [heyting_algebra α] {a b : α} (h₀ : a b = ) (h₁ : a b = ) :
a = b
@[simp]
theorem inf_compl_self {α : Type u_2} [heyting_algebra α] (a : α) :
@[simp]
theorem compl_inf_self {α : Type u_2} [heyting_algebra α] (a : α) :
theorem inf_compl_eq_bot {α : Type u_2} [heyting_algebra α] {a : α} :
theorem compl_inf_eq_bot {α : Type u_2} [heyting_algebra α] {a : α} :
@[simp]
theorem compl_top {α : Type u_2} [heyting_algebra α] :
@[simp]
theorem compl_bot {α : Type u_2} [heyting_algebra α] :
theorem le_compl_compl {α : Type u_2} [heyting_algebra α] {a : α} :
theorem compl_le_compl {α : Type u_2} [heyting_algebra α] {a b : α} (h : a b) :
@[simp]
theorem compl_compl_compl {α : Type u_2} [heyting_algebra α] (a : α) :
@[simp]
theorem disjoint_compl_compl_left_iff {α : Type u_2} [heyting_algebra α] {a b : α} :
@[simp]
theorem disjoint_compl_compl_right_iff {α : Type u_2} [heyting_algebra α] {a b : α} :
theorem compl_sup_compl_le {α : Type u_2} [heyting_algebra α] {a b : α} :
a b (a b)
theorem compl_compl_inf_distrib {α : Type u_2} [heyting_algebra α] (a b : α) :
theorem compl_compl_himp_distrib {α : Type u_2} [heyting_algebra α] (a b : α) :
@[protected, instance]
def pi.heyting_algebra {ι : Type u_1} {α : ι Type u_2} [Π (i : ι), heyting_algebra (α i)] :
heyting_algebra (Π (i : ι), α i)
Equations
@[simp]
theorem top_sdiff' {α : Type u_2} [coheyting_algebra α] (a : α) :
\ a = a
@[simp]
theorem sdiff_top {α : Type u_2} [coheyting_algebra α] (a : α) :
theorem hnot_inf_distrib {α : Type u_2} [coheyting_algebra α] (a b : α) :
(a b) = a b
theorem sdiff_le_hnot {α : Type u_2} [coheyting_algebra α] {a b : α} :
a \ b b
theorem sdiff_le_inf_hnot {α : Type u_2} [coheyting_algebra α] {a b : α} :
a \ b a b
@[simp]
theorem hnot_sdiff {α : Type u_2} [coheyting_algebra α] (a : α) :
a \ a = a
theorem hnot_sdiff_comm {α : Type u_2} [coheyting_algebra α] (a b : α) :
a \ b = b \ a
theorem hnot_le_iff_codisjoint_right {α : Type u_2} [coheyting_algebra α] {a b : α} :
theorem hnot_le_iff_codisjoint_left {α : Type u_2} [coheyting_algebra α] {a b : α} :
theorem hnot_le_comm {α : Type u_2} [coheyting_algebra α] {a b : α} :
a b b a
theorem codisjoint.hnot_le_right {α : Type u_2} [coheyting_algebra α] {a b : α} :

Alias of the reverse direction of hnot_le_iff_codisjoint_right.

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

Alias of the reverse direction of hnot_le_iff_codisjoint_left.

theorem codisjoint_hnot_right {α : Type u_2} [coheyting_algebra α] {a : α} :
theorem codisjoint_hnot_left {α : Type u_2} [coheyting_algebra α] {a : α} :
theorem has_le.le.codisjoint_hnot_left {α : Type u_2} [coheyting_algebra α] {a b : α} (h : a b) :
theorem has_le.le.codisjoint_hnot_right {α : Type u_2} [coheyting_algebra α] {a b : α} (h : b a) :
theorem is_compl.hnot_eq {α : Type u_2} [coheyting_algebra α] {a b : α} (h : is_compl a b) :
a = b
theorem is_compl.eq_hnot {α : Type u_2} [coheyting_algebra α] {a b : α} (h : is_compl a b) :
a = b
@[simp]
theorem sup_hnot_self {α : Type u_2} [coheyting_algebra α] (a : α) :
@[simp]
theorem hnot_sup_self {α : Type u_2} [coheyting_algebra α] (a : α) :
@[simp]
theorem hnot_bot {α : Type u_2} [coheyting_algebra α] :
@[simp]
theorem hnot_top {α : Type u_2} [coheyting_algebra α] :
theorem hnot_hnot_le {α : Type u_2} [coheyting_algebra α] {a : α} :
theorem hnot_le_hnot {α : Type u_2} [coheyting_algebra α] {a b : α} (h : a b) :
@[simp]
theorem hnot_hnot_hnot {α : Type u_2} [coheyting_algebra α] (a : α) :
@[simp]
theorem codisjoint_hnot_hnot_left_iff {α : Type u_2} [coheyting_algebra α] {a b : α} :
@[simp]
theorem codisjoint_hnot_hnot_right_iff {α : Type u_2} [coheyting_algebra α] {a b : α} :
theorem le_hnot_inf_hnot {α : Type u_2} [coheyting_algebra α] {a b : α} :
(a b) a b
theorem hnot_hnot_sup_distrib {α : Type u_2} [coheyting_algebra α] (a b : α) :
theorem hnot_hnot_sdiff_distrib {α : Type u_2} [coheyting_algebra α] (a b : α) :
@[simp]
@[protected, instance]
def pi.coheyting_algebra {ι : Type u_1} {α : ι Type u_2} [Π (i : ι), coheyting_algebra (α i)] :
coheyting_algebra (Π (i : ι), α i)
Equations
theorem compl_le_hnot {α : Type u_2} [biheyting_algebra α] {a : α} :
@[protected, instance]

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

Equations
@[simp]
theorem himp_iff_imp (p q : Prop) :
p q p q
@[simp]
theorem compl_iff_not (p : Prop) :
@[reducible]

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

Pullback a generalized_heyting_algebra along an injection.

Equations
@[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) :

Pullback a generalized_coheyting_algebra along an injection.

Equations
@[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) :

Pullback a heyting_algebra along an injection.

Equations
@[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) :

Pullback a coheyting_algebra along an injection.

Equations
@[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) :

Pullback a biheyting_algebra along an injection.

Equations
@[protected, instance]
Equations
@[simp]
theorem punit.top_eq  :
= punit.star
@[simp]
theorem punit.bot_eq  :
= punit.star
@[simp]
theorem punit.sup_eq (a b : punit) :
a b = punit.star
@[simp]
theorem punit.inf_eq (a b : punit) :
a b = punit.star
@[simp]
theorem punit.compl_eq (a : punit) :
a = punit.star
@[simp]
theorem punit.sdiff_eq (a b : punit) :
a \ b = punit.star
@[simp, nolint]
theorem punit.hnot_eq (a : punit) :
a = punit.star
@[simp]
theorem punit.himp_eq (a b : punit) :
a b = punit.star