Documentation

Mathlib.Order.Heyting.Basic

Heyting algebras #

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≤ b ⇨ c ↔ a ⊓ b ≤ c⇨ c ↔ a ⊓ b ≤ c↔ a ⊓ b ≤ c⊓ b ≤ c≤ 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≤ c ↔ a ≤ b ⊔ c↔ a ≤ b ⊔ c≤ b ⊔ c⊔ c and ￢a = ⊤ \ a￢a = ⊤ \ 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_1) :

Type u_1

Heyting implication ⇨⇨
himp : α → α → α

Syntax typeclass for Heyting implication ⇨⇨.

Instances

class HNot (α : Type u_1) :

Type u_1

Heyting negation ￢￢
hnot : α → α

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.

Instances

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_1) (β : Type u_2) [inst : HImp α] [inst : HImp β] :

HImp (α × β)

Equations

Prod.himp α β = { himp := fun a b => (a.fst ⇨ b.fst, a.snd ⇨ b.snd) }

instance Prod.hnot (α : Type u_1) (β : Type u_2) [inst : HNot α] [inst : HNot β] :

HNot (α × β)

Equations

Prod.hnot α β = { hnot := fun a => (￢a.fst, ￢a.snd) }

instance Prod.sdiff (α : Type u_1) (β : Type u_2) [inst : SDiff α] [inst : SDiff β] :

SDiff (α × β)

Equations

Prod.sdiff α β = { sdiff := fun a b => (a.fst \ b.fst, a.snd \ b.snd) }

instance Prod.hasCompl (α : Type u_1) (β : Type u_2) [inst : HasCompl α] [inst : HasCompl β] :

HasCompl (α × β)

Equations

Prod.hasCompl α β = { compl := fun a => (a.fstᶜ, a.sndᶜ) }

@[simp]

theorem fst_himp {α : Type u_1} {β : Type u_2} [inst : HImp α] [inst : HImp β] (a : α × β) (b : α × β) :

(a ⇨ b).fst = a.fst ⇨ b.fst

@[simp]

theorem snd_himp {α : Type u_1} {β : Type u_2} [inst : HImp α] [inst : HImp β] (a : α × β) (b : α × β) :

(a ⇨ b).snd = a.snd ⇨ b.snd

@[simp]

theorem fst_hnot {α : Type u_1} {β : Type u_2} [inst : HNot α] [inst : HNot β] (a : α × β) :

(￢a).fst = ￢a.fst

@[simp]

theorem snd_hnot {α : Type u_1} {β : Type u_2} [inst : HNot α] [inst : HNot β] (a : α × β) :

(￢a).snd = ￢a.snd

@[simp]

theorem fst_sdiff {α : Type u_1} {β : Type u_2} [inst : SDiff α] [inst : SDiff β] (a : α × β) (b : α × β) :

(a \ b).fst = a.fst \ b.fst

@[simp]

theorem snd_sdiff {α : Type u_1} {β : Type u_2} [inst : SDiff α] [inst : SDiff β] (a : α × β) (b : α × β) :

(a \ b).snd = a.snd \ b.snd

@[simp]

theorem fst_compl {α : Type u_1} {β : Type u_2} [inst : HasCompl α] [inst : HasCompl β] (a : α × β) :

aᶜ.fst = a.fstᶜ

@[simp]

theorem snd_compl {α : Type u_1} {β : Type u_2} [inst : HasCompl α] [inst : HasCompl β] (a : α × β) :

aᶜ.snd = a.sndᶜ

instance Pi.instHImpForAll {ι : Type u_1} {π : ι → Type u_2} [inst : (i : ι) → HImp (π i)] :

HImp ((i : ι) → π i)

Equations

Pi.instHImpForAll = { himp := fun a b i => a i ⇨ b i }

instance Pi.instHNotForAll {ι : Type u_1} {π : ι → Type u_2} [inst : (i : ι) → HNot (π i)] :

HNot ((i : ι) → π i)

Equations

Pi.instHNotForAll = { hnot := fun a i => ￢a i }

theorem Pi.himp_def {ι : Type u_2} {π : ι → Type u_1} [inst : (i : ι) → HImp (π i)] (a : (i : ι) → π i) (b : (i : ι) → π i) :

a ⇨ b = fun i => a i ⇨ b i

theorem Pi.hnot_def {ι : Type u_2} {π : ι → Type u_1} [inst : (i : ι) → HNot (π i)] (a : (i : ι) → π i) :

￢a = fun i => ￢a i

@[simp]

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

(((i : ι) → π i) ⇨ Pi.instHImpForAll) a b i = a i ⇨ b i

@[simp]

theorem Pi.hnot_apply {ι : Type u_2} {π : ι → Type u_1} [inst : (i : ι) → HNot (π i)] (a : (i : ι) → π i) (i : ι) :

(￢((i : ι) → π i)) Pi.instHNotForAll a i = ￢a i

class GeneralizedHeytingAlgebra (α : Type u_1) extends Lattice , Top , HImp :

Type u_1

⊤⊤ is a greatest element
le_top : ∀ (a : α), a ≤ ⊤
a ⇨⇨ is right adjoint to a ⊓⊓
le_himp_iff : ∀ (a b c : α), a ≤ b ⇨ c ↔ a ⊓ b ≤ c

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.

Instances

class GeneralizedCoheytingAlgebra (α : Type u_1) extends Lattice , Bot , SDiff :

Type u_1

⊥⊥ is a least element
bot_le : ∀ (a : α), ⊥ ≤ a
\ a is right adjoint to ⊔ a⊔ a
sdiff_le_iff : ∀ (a b c : α), a \ b ≤ c ↔ a ≤ b ⊔ c

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

This generalizes CoheytingAlgebra by not requiring a top element.

Instances

class HeytingAlgebra (α : Type u_1) extends GeneralizedHeytingAlgebra , Bot , HasCompl :

Type u_1

⊥⊥ is a least element
bot_le : ∀ (a : α), ⊥ ≤ a
a ⇨⇨ is right adjoint to a ⊓⊓
himp_bot : ∀ (a : α), a ⇨ ⊥ = aᶜ

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

Instances

class CoheytingAlgebra (α : Type u_1) extends GeneralizedCoheytingAlgebra , Top , HNot :

Type u_1

⊤⊤ is a greatest element
le_top : ∀ (a : α), a ≤ ⊤
⊤ \ a⊤ \ a is ￢a￢a
top_sdiff : ∀ (a : α), ⊤ \ a = ￢a

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

Instances

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

Type u_1

\ a is right adjoint to ⊔ a⊔ a
sdiff_le_iff : ∀ (a b c : α), a \ b ≤ c ↔ a ≤ b ⊔ c
⊤ \ a⊤ \ a is ￢a￢a
top_sdiff : ∀ (a : α), ⊤ \ a = ￢a

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

Instances

instance GeneralizedHeytingAlgebra.toOrderTop {α : Type u_1} [inst : GeneralizedHeytingAlgebra α] :

Equations

GeneralizedHeytingAlgebra.toOrderTop = let src := inst; OrderTop.mk (_ : ∀ (a : α), a ≤ ⊤)

instance GeneralizedCoheytingAlgebra.toOrderBot {α : Type u_1} [inst : GeneralizedCoheytingAlgebra α] :

Equations

GeneralizedCoheytingAlgebra.toOrderBot = let src := inst; OrderBot.mk (_ : ∀ (a : α), ⊥ ≤ a)

instance HeytingAlgebra.toBoundedOrder {α : Type u_1} [inst : HeytingAlgebra α] :

BoundedOrder α

Equations

HeytingAlgebra.toBoundedOrder = BoundedOrder.mk

instance CoheytingAlgebra.toBoundedOrder {α : Type u_1} [inst : CoheytingAlgebra α] :

BoundedOrder α

Equations

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

instance BiheytingAlgebra.toCoheytingAlgebra {α : Type u_1} [inst : BiheytingAlgebra α] :

CoheytingAlgebra α

Equations

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

def HeytingAlgebra.ofHImp {α : Type u_1} [inst : DistribLattice α] [inst : 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 : α), a ⇨ ⊥ = a ⇨ ⊥)

def HeytingAlgebra.ofCompl {α : Type u_1} [inst : DistribLattice α] [inst : 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 : α), ⊥ ≤ a) (_ : ∀ (a : α), compl a ⊔ ⊥ = compl a)

def CoheytingAlgebra.ofSDiff {α : Type u_1} [inst : DistribLattice α] [inst : 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 : α), ⊤ \ a = ⊤ \ a)

def CoheytingAlgebra.ofHNot {α : Type u_1} [inst : DistribLattice α] [inst : 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 : α), a ≤ ⊤) (_ : ∀ (a : α), ⊤ ⊓ hnot a = hnot a)

@[simp]

theorem le_himp_iff {α : Type u_1} [inst : GeneralizedHeytingAlgebra α] {a : α} {b : α} {c : α} :

a ≤ b ⇨ c ↔ a ⊓ b ≤ c

theorem le_himp_iff' {α : Type u_1} [inst : GeneralizedHeytingAlgebra α] {a : α} {b : α} {c : α} :

a ≤ b ⇨ c ↔ b ⊓ a ≤ c

theorem le_himp_comm {α : Type u_1} [inst : GeneralizedHeytingAlgebra α] {a : α} {b : α} {c : α} :

a ≤ b ⇨ c ↔ b ≤ a ⇨ c

theorem le_himp {α : Type u_1} [inst : GeneralizedHeytingAlgebra α] {a : α} {b : α} :

a ≤ b ⇨ a

theorem le_himp_iff_left {α : Type u_1} [inst : GeneralizedHeytingAlgebra α] {a : α} {b : α} :

a ≤ a ⇨ b ↔ a ≤ b

@[simp]

theorem himp_self {α : Type u_1} [inst : GeneralizedHeytingAlgebra α] {a : α} :

theorem himp_inf_le {α : Type u_1} [inst : GeneralizedHeytingAlgebra α] {a : α} {b : α} :

(a ⇨ b) ⊓ a ≤ b

theorem inf_himp_le {α : Type u_1} [inst : GeneralizedHeytingAlgebra α] {a : α} {b : α} :

a ⊓ (a ⇨ b) ≤ b

@[simp]

theorem inf_himp {α : Type u_1} [inst : GeneralizedHeytingAlgebra α] (a : α) (b : α) :

a ⊓ (a ⇨ b) = a ⊓ b

@[simp]

theorem himp_inf_self {α : Type u_1} [inst : GeneralizedHeytingAlgebra α] (a : α) (b : α) :

(a ⇨ b) ⊓ a = b ⊓ a

@[simp]

theorem himp_eq_top_iff {α : Type u_1} [inst : 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_1} [inst : GeneralizedHeytingAlgebra α] {a : α} :

a ⇨ ⊤ = ⊤

@[simp]

theorem top_himp {α : Type u_1} [inst : GeneralizedHeytingAlgebra α] {a : α} :

theorem himp_himp {α : Type u_1} [inst : GeneralizedHeytingAlgebra α] (a : α) (b : α) (c : α) :

a ⇨ b ⇨ c = a ⊓ b ⇨ c

theorem himp_le_himp_himp_himp {α : Type u_1} [inst : GeneralizedHeytingAlgebra α] {a : α} {b : α} {c : α} :

b ⇨ c ≤ (a ⇨ b) ⇨ a ⇨ c

@[simp]

theorem himp_inf_himp_inf_le {α : Type u_1} [inst : GeneralizedHeytingAlgebra α] {a : α} {b : α} {c : α} :

(b ⇨ c) ⊓ (a ⇨ b) ⊓ a ≤ c

theorem himp_left_comm {α : Type u_1} [inst : GeneralizedHeytingAlgebra α] (a : α) (b : α) (c : α) :

a ⇨ b ⇨ c = b ⇨ a ⇨ c

@[simp]

theorem himp_idem {α : Type u_1} [inst : GeneralizedHeytingAlgebra α] {a : α} {b : α} :

b ⇨ b ⇨ a = b ⇨ a

theorem himp_inf_distrib {α : Type u_1} [inst : GeneralizedHeytingAlgebra α] (a : α) (b : α) (c : α) :

a ⇨ b ⊓ c = (a ⇨ b) ⊓ (a ⇨ c)

theorem sup_himp_distrib {α : Type u_1} [inst : GeneralizedHeytingAlgebra α] (a : α) (b : α) (c : α) :

a ⊔ b ⇨ c = (a ⇨ c) ⊓ (b ⇨ c)

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

c ⇨ a ≤ c ⇨ b

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

b ⇨ c ≤ a ⇨ c

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

b ⇨ c ≤ a ⇨ d

@[simp]

theorem sup_himp_self_left {α : Type u_1} [inst : GeneralizedHeytingAlgebra α] (a : α) (b : α) :

a ⊔ b ⇨ a = b ⇨ a

@[simp]

theorem sup_himp_self_right {α : Type u_1} [inst : GeneralizedHeytingAlgebra α] (a : α) (b : α) :

a ⊔ b ⇨ b = a ⇨ b

theorem Codisjoint.himp_eq_right {α : Type u_1} [inst : GeneralizedHeytingAlgebra α] {a : α} {b : α} (h : Codisjoint a b) :

b ⇨ a = a

theorem Codisjoint.himp_eq_left {α : Type u_1} [inst : GeneralizedHeytingAlgebra α] {a : α} {b : α} (h : Codisjoint a b) :

a ⇨ b = b

theorem Codisjoint.himp_inf_cancel_right {α : Type u_1} [inst : GeneralizedHeytingAlgebra α] {a : α} {b : α} (h : Codisjoint a b) :

a ⇨ a ⊓ b = b

theorem Codisjoint.himp_inf_cancel_left {α : Type u_1} [inst : GeneralizedHeytingAlgebra α] {a : α} {b : α} (h : Codisjoint a b) :

b ⇨ a ⊓ b = a

theorem le_himp_himp {α : Type u_1} [inst : GeneralizedHeytingAlgebra α] {a : α} {b : α} :

a ≤ (a ⇨ b) ⇨ b

theorem himp_triangle {α : Type u_1} [inst : GeneralizedHeytingAlgebra α] (a : α) (b : α) (c : α) :

(a ⇨ b) ⊓ (b ⇨ c) ≤ a ⇨ c

theorem himp_inf_himp_cancel {α : Type u_1} [inst : GeneralizedHeytingAlgebra α] {a : α} {b : α} {c : α} (hba : b ≤ a) (hcb : c ≤ b) :

(a ⇨ b) ⊓ (b ⇨ c) = a ⇨ c

instance GeneralizedHeytingAlgebra.toDistribLattice {α : Type u_1} [inst : GeneralizedHeytingAlgebra α] :

DistribLattice α

Equations

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

instance instGeneralizedCoheytingAlgebraOrderDual {α : Type u_1} [inst : GeneralizedHeytingAlgebra α] :

GeneralizedCoheytingAlgebra αᵒᵈ

Equations

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

instance Prod.generalizedHeytingAlgebra {α : Type u_1} {β : Type u_2} [inst : GeneralizedHeytingAlgebra α] [inst : GeneralizedHeytingAlgebra β] :

GeneralizedHeytingAlgebra (α × β)

Equations

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

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

GeneralizedHeytingAlgebra ((i : ι) → α i)

Equations

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

@[simp]

theorem sdiff_le_iff {α : Type u_1} [inst : GeneralizedCoheytingAlgebra α] {a : α} {b : α} {c : α} :

a \ b ≤ c ↔ a ≤ b ⊔ c

theorem sdiff_le_iff' {α : Type u_1} [inst : GeneralizedCoheytingAlgebra α] {a : α} {b : α} {c : α} :

a \ b ≤ c ↔ a ≤ c ⊔ b

theorem sdiff_le_comm {α : Type u_1} [inst : GeneralizedCoheytingAlgebra α] {a : α} {b : α} {c : α} :

a \ b ≤ c ↔ a \ c ≤ b

theorem sdiff_le {α : Type u_1} [inst : GeneralizedCoheytingAlgebra α] {a : α} {b : α} :

a \ b ≤ a

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

Disjoint (a \ c) b

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

Disjoint a (b \ c)

theorem sdiff_le_iff_left {α : Type u_1} [inst : GeneralizedCoheytingAlgebra α] {a : α} {b : α} :

a \ b ≤ b ↔ a ≤ b

@[simp]

theorem sdiff_self {α : Type u_1} [inst : GeneralizedCoheytingAlgebra α] {a : α} :

a \ a = ⊥

theorem le_sup_sdiff {α : Type u_1} [inst : GeneralizedCoheytingAlgebra α] {a : α} {b : α} :

a ≤ b ⊔ a \ b

theorem le_sdiff_sup {α : Type u_1} [inst : GeneralizedCoheytingAlgebra α] {a : α} {b : α} :

a ≤ a \ b ⊔ b

theorem sup_sdiff_left {α : Type u_1} [inst : GeneralizedCoheytingAlgebra α] {a : α} {b : α} :

a ⊔ a \ b = a

theorem sup_sdiff_right {α : Type u_1} [inst : GeneralizedCoheytingAlgebra α] {a : α} {b : α} :

a \ b ⊔ a = a

theorem inf_sdiff_left {α : Type u_1} [inst : GeneralizedCoheytingAlgebra α] {a : α} {b : α} :

a \ b ⊓ a = a \ b

theorem inf_sdiff_right {α : Type u_1} [inst : GeneralizedCoheytingAlgebra α] {a : α} {b : α} :

a ⊓ a \ b = a \ b

@[simp]

theorem sup_sdiff_self {α : Type u_1} [inst : GeneralizedCoheytingAlgebra α] (a : α) (b : α) :

a ⊔ b \ a = a ⊔ b

@[simp]

theorem sdiff_sup_self {α : Type u_1} [inst : GeneralizedCoheytingAlgebra α] (a : α) (b : α) :

b \ a ⊔ a = b ⊔ a

theorem sup_sdiff_self_left {α : Type u_1} [inst : GeneralizedCoheytingAlgebra α] (a : α) (b : α) :

b \ a ⊔ a = b ⊔ a

Alias of sdiff_sup_self.

theorem sup_sdiff_self_right {α : Type u_1} [inst : GeneralizedCoheytingAlgebra α] (a : α) (b : α) :

a ⊔ b \ a = a ⊔ b

Alias of sup_sdiff_self.

theorem sup_sdiff_eq_sup {α : Type u_1} [inst : GeneralizedCoheytingAlgebra α] {a : α} {b : α} {c : α} (h : c ≤ a) :

a ⊔ b \ c = a ⊔ b

theorem sup_sdiff_cancel' {α : Type u_1} [inst : GeneralizedCoheytingAlgebra α] {a : α} {b : α} {c : α} (hab : a ≤ b) (hbc : b ≤ c) :

b ⊔ c \ a = c

theorem sup_sdiff_cancel_right {α : Type u_1} [inst : GeneralizedCoheytingAlgebra α] {a : α} {b : α} (h : a ≤ b) :

a ⊔ b \ a = b

theorem sdiff_sup_cancel {α : Type u_1} [inst : GeneralizedCoheytingAlgebra α] {a : α} {b : α} (h : b ≤ a) :

a \ b ⊔ b = a

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

a ⊔ b ≤ c

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

a ⊔ b ≤ c

@[simp]

theorem sdiff_eq_bot_iff {α : Type u_1} [inst : GeneralizedCoheytingAlgebra α] {a : α} {b : α} :

a \ b = ⊥ ↔ a ≤ b

@[simp]

theorem sdiff_bot {α : Type u_1} [inst : GeneralizedCoheytingAlgebra α] {a : α} :

a \ ⊥ = a

@[simp]

theorem bot_sdiff {α : Type u_1} [inst : GeneralizedCoheytingAlgebra α] {a : α} :

theorem sdiff_sdiff_sdiff_le_sdiff {α : Type u_1} [inst : GeneralizedCoheytingAlgebra α] {a : α} {b : α} {c : α} :

(a \ b) \ (a \ c) ≤ c \ b

@[simp]

theorem le_sup_sdiff_sup_sdiff {α : Type u_1} [inst : GeneralizedCoheytingAlgebra α] {a : α} {b : α} {c : α} :

a ≤ b ⊔ (a \ c ⊔ c \ b)

theorem sdiff_sdiff {α : Type u_1} [inst : GeneralizedCoheytingAlgebra α] (a : α) (b : α) (c : α) :

(a \ b) \ c = a \ (b ⊔ c)

theorem sdiff_sdiff_left {α : Type u_1} [inst : GeneralizedCoheytingAlgebra α] {a : α} {b : α} {c : α} :

(a \ b) \ c = a \ (b ⊔ c)

theorem sdiff_right_comm {α : Type u_1} [inst : GeneralizedCoheytingAlgebra α] (a : α) (b : α) (c : α) :

(a \ b) \ c = (a \ c) \ b

theorem sdiff_sdiff_comm {α : Type u_1} [inst : GeneralizedCoheytingAlgebra α] {a : α} {b : α} {c : α} :

(a \ b) \ c = (a \ c) \ b

@[simp]

theorem sdiff_idem {α : Type u_1} [inst : GeneralizedCoheytingAlgebra α] {a : α} {b : α} :

(a \ b) \ b = a \ b

@[simp]

theorem sdiff_sdiff_self {α : Type u_1} [inst : GeneralizedCoheytingAlgebra α] {a : α} {b : α} :

(a \ b) \ a = ⊥

theorem sup_sdiff_distrib {α : Type u_1} [inst : GeneralizedCoheytingAlgebra α] (a : α) (b : α) (c : α) :

(a ⊔ b) \ c = a \ c ⊔ b \ c

theorem sdiff_inf_distrib {α : Type u_1} [inst : GeneralizedCoheytingAlgebra α] (a : α) (b : α) (c : α) :

a \ (b ⊓ c) = a \ b ⊔ a \ c

theorem sup_sdiff {α : Type u_1} [inst : GeneralizedCoheytingAlgebra α] {a : α} {b : α} {c : α} :

(a ⊔ b) \ c = a \ c ⊔ b \ c

@[simp]

theorem sup_sdiff_right_self {α : Type u_1} [inst : GeneralizedCoheytingAlgebra α] {a : α} {b : α} :

(a ⊔ b) \ b = a \ b

@[simp]

theorem sup_sdiff_left_self {α : Type u_1} [inst : GeneralizedCoheytingAlgebra α] {a : α} {b : α} :

(a ⊔ b) \ a = b \ a

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

a \ c ≤ b \ c

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

c \ b ≤ c \ a

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

a \ d ≤ b \ c

theorem sdiff_inf {α : Type u_1} [inst : GeneralizedCoheytingAlgebra α] {a : α} {b : α} {c : α} :

a \ (b ⊓ c) = a \ b ⊔ a \ c

@[simp]

theorem sdiff_inf_self_left {α : Type u_1} [inst : GeneralizedCoheytingAlgebra α] (a : α) (b : α) :

a \ (a ⊓ b) = a \ b

@[simp]

theorem sdiff_inf_self_right {α : Type u_1} [inst : GeneralizedCoheytingAlgebra α] (a : α) (b : α) :

b \ (a ⊓ b) = b \ a

theorem Disjoint.sdiff_eq_left {α : Type u_1} [inst : GeneralizedCoheytingAlgebra α] {a : α} {b : α} (h : Disjoint a b) :

a \ b = a

theorem Disjoint.sdiff_eq_right {α : Type u_1} [inst : GeneralizedCoheytingAlgebra α] {a : α} {b : α} (h : Disjoint a b) :

b \ a = b

theorem Disjoint.sup_sdiff_cancel_left {α : Type u_1} [inst : GeneralizedCoheytingAlgebra α] {a : α} {b : α} (h : Disjoint a b) :

(a ⊔ b) \ a = b

theorem Disjoint.sup_sdiff_cancel_right {α : Type u_1} [inst : GeneralizedCoheytingAlgebra α] {a : α} {b : α} (h : Disjoint a b) :

(a ⊔ b) \ b = a

theorem sdiff_sdiff_le {α : Type u_1} [inst : GeneralizedCoheytingAlgebra α] {a : α} {b : α} :

a \ (a \ b) ≤ b

theorem sdiff_triangle {α : Type u_1} [inst : GeneralizedCoheytingAlgebra α] (a : α) (b : α) (c : α) :

a \ c ≤ a \ b ⊔ b \ c

theorem sdiff_sup_sdiff_cancel {α : Type u_1} [inst : 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_1} [inst : GeneralizedCoheytingAlgebra α] {a : α} {b : α} {c : α} (h : c ⊔ a ≤ c ⊔ b) :

a \ c ≤ b \ c

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

a \ c ≤ b \ c

@[simp]

theorem inf_sdiff_sup_left {α : Type u_1} [inst : GeneralizedCoheytingAlgebra α] {a : α} {b : α} {c : α} :

a \ c ⊓ (a ⊔ b) = a \ c

@[simp]

theorem inf_sdiff_sup_right {α : Type u_1} [inst : GeneralizedCoheytingAlgebra α] {a : α} {b : α} {c : α} :

a \ c ⊓ (b ⊔ a) = a \ c

instance GeneralizedCoheytingAlgebra.toDistribLattice {α : Type u_1} [inst : GeneralizedCoheytingAlgebra α] :

DistribLattice α

Equations

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

instance instGeneralizedHeytingAlgebraOrderDual {α : Type u_1} [inst : GeneralizedCoheytingAlgebra α] :

GeneralizedHeytingAlgebra αᵒᵈ

Equations

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

instance Prod.generalizedCoheytingAlgebra {α : Type u_1} {β : Type u_2} [inst : GeneralizedCoheytingAlgebra α] [inst : GeneralizedCoheytingAlgebra β] :

GeneralizedCoheytingAlgebra (α × β)

Equations

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

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

GeneralizedCoheytingAlgebra ((i : ι) → α i)

Equations

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

@[simp]

theorem himp_bot {α : Type u_1} [inst : HeytingAlgebra α] (a : α) :

a ⇨ ⊥ = aᶜ

@[simp]

theorem bot_himp {α : Type u_1} [inst : HeytingAlgebra α] (a : α) :

⊥ ⇨ a = ⊤

theorem compl_sup_distrib {α : Type u_1} [inst : HeytingAlgebra α] (a : α) (b : α) :

(a ⊔ b)ᶜ = aᶜ ⊓ bᶜ

@[simp]

theorem compl_sup {α : Type u_1} [inst : HeytingAlgebra α] {a : α} {b : α} :

(a ⊔ b)ᶜ = aᶜ ⊓ bᶜ

theorem compl_le_himp {α : Type u_1} [inst : HeytingAlgebra α] {a : α} {b : α} :

aᶜ ≤ a ⇨ b

theorem compl_sup_le_himp {α : Type u_1} [inst : HeytingAlgebra α] {a : α} {b : α} :

aᶜ ⊔ b ≤ a ⇨ b

theorem sup_compl_le_himp {α : Type u_1} [inst : HeytingAlgebra α] {a : α} {b : α} :

b ⊔ aᶜ ≤ a ⇨ b

@[simp]

theorem himp_compl {α : Type u_1} [inst : HeytingAlgebra α] (a : α) :

a ⇨ aᶜ = aᶜ

theorem himp_compl_comm {α : Type u_1} [inst : HeytingAlgebra α] (a : α) (b : α) :

a ⇨ bᶜ = b ⇨ aᶜ

theorem le_compl_iff_disjoint_right {α : Type u_1} [inst : HeytingAlgebra α] {a : α} {b : α} :

a ≤ bᶜ ↔ Disjoint a b

theorem le_compl_iff_disjoint_left {α : Type u_1} [inst : HeytingAlgebra α] {a : α} {b : α} :

a ≤ bᶜ ↔ Disjoint b a

theorem le_compl_comm {α : Type u_1} [inst : HeytingAlgebra α] {a : α} {b : α} :

a ≤ bᶜ ↔ b ≤ aᶜ

theorem Disjoint.le_compl_right {α : Type u_1} [inst : 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_1} [inst : 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_1} [inst : HeytingAlgebra α] {a : α} {b : α} :

a ≤ bᶜ ↔ b ≤ aᶜ

Alias of le_compl_comm.

theorem le_compl_of_le_compl {α : Type u_1} [inst : HeytingAlgebra α] {a : α} {b : α} :

a ≤ bᶜ → b ≤ aᶜ

Alias of the forward direction of le_compl_comm.

theorem disjoint_compl_left {α : Type u_1} [inst : HeytingAlgebra α] {a : α} :

Disjoint (aᶜ) a

theorem disjoint_compl_right {α : Type u_1} [inst : HeytingAlgebra α] {a : α} :

Disjoint a (aᶜ)

theorem LE.le.disjoint_compl_left {α : Type u_1} [inst : HeytingAlgebra α] {a : α} {b : α} (h : b ≤ a) :

Disjoint (aᶜ) b

theorem LE.le.disjoint_compl_right {α : Type u_1} [inst : HeytingAlgebra α] {a : α} {b : α} (h : a ≤ b) :

Disjoint a (bᶜ)

theorem IsCompl.compl_eq {α : Type u_1} [inst : HeytingAlgebra α] {a : α} {b : α} (h : IsCompl a b) :

aᶜ = b

theorem IsCompl.eq_compl {α : Type u_1} [inst : HeytingAlgebra α] {a : α} {b : α} (h : IsCompl a b) :

a = bᶜ

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

aᶜ = b

@[simp]

theorem inf_compl_self {α : Type u_1} [inst : HeytingAlgebra α] (a : α) :

a ⊓ aᶜ = ⊥

@[simp]

theorem compl_inf_self {α : Type u_1} [inst : HeytingAlgebra α] (a : α) :

aᶜ ⊓ a = ⊥

theorem inf_compl_eq_bot {α : Type u_1} [inst : HeytingAlgebra α] {a : α} :

a ⊓ aᶜ = ⊥

theorem compl_inf_eq_bot {α : Type u_1} [inst : HeytingAlgebra α] {a : α} :

aᶜ ⊓ a = ⊥

@[simp]

theorem compl_top {α : Type u_1} [inst : HeytingAlgebra α] :

@[simp]

theorem compl_bot {α : Type u_1} [inst : HeytingAlgebra α] :

theorem le_compl_compl {α : Type u_1} [inst : HeytingAlgebra α] {a : α} :

theorem compl_anti {α : Type u_1} [inst : HeytingAlgebra α] :

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

@[simp]

theorem compl_compl_compl {α : Type u_1} [inst : HeytingAlgebra α] (a : α) :

aᶜᶜᶜ = aᶜ

@[simp]

theorem disjoint_compl_compl_left_iff {α : Type u_1} [inst : HeytingAlgebra α] {a : α} {b : α} :

Disjoint (aᶜᶜ) b ↔ Disjoint a b

@[simp]

theorem disjoint_compl_compl_right_iff {α : Type u_1} [inst : HeytingAlgebra α] {a : α} {b : α} :

Disjoint a (bᶜᶜ) ↔ Disjoint a b

theorem compl_sup_compl_le {α : Type u_1} [inst : HeytingAlgebra α] {a : α} {b : α} :

aᶜ ⊔ bᶜ ≤ (a ⊓ b)ᶜ

theorem compl_compl_inf_distrib {α : Type u_1} [inst : HeytingAlgebra α] (a : α) (b : α) :

(a ⊓ b)ᶜᶜ = aᶜᶜ ⊓ bᶜᶜ

theorem compl_compl_himp_distrib {α : Type u_1} [inst : HeytingAlgebra α] (a : α) (b : α) :

(a ⇨ b)ᶜᶜ = aᶜᶜ ⇨ bᶜᶜ

instance instCoheytingAlgebraOrderDual {α : Type u_1} [inst : HeytingAlgebra α] :

CoheytingAlgebra αᵒᵈ

Equations

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

@[simp]

theorem ofDual_hnot {α : Type u_1} [inst : HeytingAlgebra α] (a : αᵒᵈ) :

↑OrderDual.ofDual (￢a) = ↑OrderDual.ofDual aᶜ

@[simp]

theorem toDual_compl {α : Type u_1} [inst : HeytingAlgebra α] (a : α) :

↑OrderDual.toDual (aᶜ) = ￢↑OrderDual.toDual a

instance Prod.heytingAlgebra {α : Type u_1} {β : Type u_2} [inst : HeytingAlgebra α] [inst : HeytingAlgebra β] :

HeytingAlgebra (α × β)

Equations

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

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

HeytingAlgebra ((i : ι) → α i)

Equations

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

@[simp]

theorem top_sdiff' {α : Type u_1} [inst : CoheytingAlgebra α] (a : α) :

@[simp]

theorem sdiff_top {α : Type u_1} [inst : CoheytingAlgebra α] (a : α) :

theorem hnot_inf_distrib {α : Type u_1} [inst : CoheytingAlgebra α] (a : α) (b : α) :

￢(a ⊓ b) = ￢a ⊔ ￢b

theorem sdiff_le_hnot {α : Type u_1} [inst : CoheytingAlgebra α] {a : α} {b : α} :

a \ b ≤ ￢b

theorem sdiff_le_inf_hnot {α : Type u_1} [inst : CoheytingAlgebra α] {a : α} {b : α} :

a \ b ≤ a ⊓ ￢b

instance CoheytingAlgebra.toDistribLattice {α : Type u_1} [inst : 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_1} [inst : CoheytingAlgebra α] (a : α) :

￢a \ a = ￢a

theorem hnot_sdiff_comm {α : Type u_1} [inst : CoheytingAlgebra α] (a : α) (b : α) :

￢a \ b = ￢b \ a

theorem hnot_le_iff_codisjoint_right {α : Type u_1} [inst : CoheytingAlgebra α] {a : α} {b : α} :

￢a ≤ b ↔ Codisjoint a b

theorem hnot_le_iff_codisjoint_left {α : Type u_1} [inst : CoheytingAlgebra α] {a : α} {b : α} :

￢a ≤ b ↔ Codisjoint b a

theorem hnot_le_comm {α : Type u_1} [inst : CoheytingAlgebra α] {a : α} {b : α} :

￢a ≤ b ↔ ￢b ≤ a

theorem Codisjoint.hnot_le_right {α : Type u_1} [inst : 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_1} [inst : 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_1} [inst : CoheytingAlgebra α] {a : α} :

Codisjoint a (￢a)

theorem codisjoint_hnot_left {α : Type u_1} [inst : CoheytingAlgebra α] {a : α} :

Codisjoint (￢a) a

theorem LE.le.codisjoint_hnot_left {α : Type u_1} [inst : CoheytingAlgebra α] {a : α} {b : α} (h : a ≤ b) :

Codisjoint (￢a) b

theorem LE.le.codisjoint_hnot_right {α : Type u_1} [inst : CoheytingAlgebra α] {a : α} {b : α} (h : b ≤ a) :

Codisjoint a (￢b)

theorem IsCompl.hnot_eq {α : Type u_1} [inst : CoheytingAlgebra α] {a : α} {b : α} (h : IsCompl a b) :

￢a = b

theorem IsCompl.eq_hnot {α : Type u_1} [inst : CoheytingAlgebra α] {a : α} {b : α} (h : IsCompl a b) :

a = ￢b

@[simp]

theorem sup_hnot_self {α : Type u_1} [inst : CoheytingAlgebra α] (a : α) :

a ⊔ ￢a = ⊤

@[simp]

theorem hnot_sup_self {α : Type u_1} [inst : CoheytingAlgebra α] (a : α) :

￢a ⊔ a = ⊤

@[simp]

theorem hnot_bot {α : Type u_1} [inst : CoheytingAlgebra α] :

@[simp]

theorem hnot_top {α : Type u_1} [inst : CoheytingAlgebra α] :

theorem hnot_hnot_le {α : Type u_1} [inst : CoheytingAlgebra α] {a : α} :

theorem hnot_anti {α : Type u_1} [inst : CoheytingAlgebra α] :

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

@[simp]

theorem hnot_hnot_hnot {α : Type u_1} [inst : CoheytingAlgebra α] (a : α) :

￢￢￢a = ￢a

@[simp]

theorem codisjoint_hnot_hnot_left_iff {α : Type u_1} [inst : CoheytingAlgebra α] {a : α} {b : α} :

Codisjoint (￢￢a) b ↔ Codisjoint a b

@[simp]

theorem codisjoint_hnot_hnot_right_iff {α : Type u_1} [inst : CoheytingAlgebra α] {a : α} {b : α} :

Codisjoint a (￢￢b) ↔ Codisjoint a b

theorem le_hnot_inf_hnot {α : Type u_1} [inst : CoheytingAlgebra α] {a : α} {b : α} :

￢(a ⊔ b) ≤ ￢a ⊓ ￢b

theorem hnot_hnot_sup_distrib {α : Type u_1} [inst : CoheytingAlgebra α] (a : α) (b : α) :

￢￢(a ⊔ b) = ￢￢a ⊔ ￢￢b

theorem hnot_hnot_sdiff_distrib {α : Type u_1} [inst : CoheytingAlgebra α] (a : α) (b : α) :

￢￢(a \ b) = ￢￢a \ ￢￢b

instance instHeytingAlgebraOrderDual {α : Type u_1} [inst : CoheytingAlgebra α] :

HeytingAlgebra αᵒᵈ

Equations

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

@[simp]

theorem ofDual_compl {α : Type u_1} [inst : CoheytingAlgebra α] (a : αᵒᵈ) :

↑OrderDual.ofDual (aᶜ) = ￢↑OrderDual.ofDual a

@[simp]

theorem ofDual_himp {α : Type u_1} [inst : CoheytingAlgebra α] (a : αᵒᵈ) (b : αᵒᵈ) :

↑OrderDual.ofDual (a ⇨ b) = ↑OrderDual.ofDual b \ ↑OrderDual.ofDual a

@[simp]

theorem toDual_hnot {α : Type u_1} [inst : CoheytingAlgebra α] (a : α) :

↑OrderDual.toDual (￢a) = ↑OrderDual.toDual aᶜ

@[simp]

theorem toDual_sdiff {α : Type u_1} [inst : CoheytingAlgebra α] (a : α) (b : α) :

↑OrderDual.toDual (a \ b) = ↑OrderDual.toDual b ⇨ ↑OrderDual.toDual a

instance Prod.coheytingAlgebra {α : Type u_1} {β : Type u_2} [inst : CoheytingAlgebra α] [inst : CoheytingAlgebra β] :

CoheytingAlgebra (α × β)

Equations

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

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

CoheytingAlgebra ((i : ι) → α i)

Equations

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

theorem compl_le_hnot {α : Type u_1} [inst : BiheytingAlgebra α] {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_3 Prop.heytingAlgebra.proof_4

@[simp]

theorem himp_iff_imp (p : Prop) (q : Prop) :

p ⇨ q ↔ p → q

@[simp]

theorem compl_iff_not (p : Prop) :

def LinearOrder.toBiheytingAlgebra {α : Type u_1} [inst : LinearOrder α] [inst : BoundedOrder α] :

BiheytingAlgebra α

A bounded linear order is a bi-Heyting algebra by setting

a ⇨ b = ⊤⇨ b = ⊤⊤ if a ≤ b≤ b and a ⇨ b = b⇨ b = b otherwise.
a \ b = ⊥⊥ if a ≤ b≤ b and a \ b = a otherwise.

Equations

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

def Function.Injective.generalizedHeytingAlgebra {α : Type u_1} {β : Type u_2} [inst : Sup α] [inst : Inf α] [inst : Top α] [inst : HImp α] [inst : 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.

def Function.Injective.generalizedCoheytingAlgebra {α : Type u_1} {β : Type u_2} [inst : Sup α] [inst : Inf α] [inst : Bot α] [inst : SDiff α] [inst : 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.

def Function.Injective.heytingAlgebra {α : Type u_1} {β : Type u_2} [inst : Sup α] [inst : Inf α] [inst : Top α] [inst : Bot α] [inst : HasCompl α] [inst : HImp α] [inst : 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.

def Function.Injective.coheytingAlgebra {α : Type u_1} {β : Type u_2} [inst : Sup α] [inst : Inf α] [inst : Top α] [inst : Bot α] [inst : HNot α] [inst : SDiff α] [inst : 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.

def Function.Injective.biheytingAlgebra {α : Type u_1} {β : Type u_2} [inst : Sup α] [inst : Inf α] [inst : Top α] [inst : Bot α] [inst : HasCompl α] [inst : HNot α] [inst : HImp α] [inst : SDiff α] [inst : 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

Equations

PUnit.biheytingAlgebra = let src := PUnit.linearOrder; BiheytingAlgebra.mk PUnit.biheytingAlgebra.proof_11 PUnit.biheytingAlgebra.proof_12

@[simp]

theorem PUnit.top_eq :

⊤ = PUnit.unit

@[simp]

theorem PUnit.bot_eq :

⊥ = PUnit.unit

@[simp]

theorem PUnit.sup_eq (a : PUnit) (b : PUnit) :

a ⊔ b = PUnit.unit

@[simp]

theorem PUnit.inf_eq (a : PUnit) (b : PUnit) :

a ⊓ b = PUnit.unit

@[simp]

theorem PUnit.compl_eq (a : PUnit) :

aᶜ = PUnit.unit

@[simp]

theorem PUnit.sdiff_eq (a : PUnit) (b : PUnit) :

a \ b = PUnit.unit

@[simp]

theorem PUnit.hnot_eq (a : PUnit) :

￢a = PUnit.unit

@[simp]

theorem PUnit.himp_eq (a : PUnit) (b : PUnit) :

a ⇨ b = PUnit.unit