Documentation

Mathlib.Order.Heyting.Basic

Heyting algebras #

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

A Heyting algebra is a bounded distributive lattice with an implication operation such that a ≤ b ⇨ c ↔ a ⊓ b ≤ c. It also comes with a pseudo-complement , such that aᶜ = a ⇨ ⊥.

Co-Heyting algebras are dual to Heyting algebras. They have a difference \ and a negation such that a \ b ≤ c ↔ a ≤ b ⊔ c and ¬a = ⊤ \ a.

Bi-Heyting algebras are Heyting algebras that are also co-Heyting algebras.

From a logic standpoint, Heyting algebras precisely model intuitionistic logic, whereas boolean algebras model classical logic.

Heyting algebras are the order theoretic equivalent of cartesian-closed categories.

Main declarations #

References #

Tags #

Heyting, Brouwer, algebra, implication, negation, intuitionistic

Notation #

instance Prod.instHImp (α : Type u_2) (β : Type u_3) [HImp α] [HImp β] :
HImp (α × β)
Equations
instance Prod.instHNot (α : Type u_2) (β : Type u_3) [HNot α] [HNot β] :
HNot (α × β)
Equations
instance Prod.instSDiff (α : Type u_2) (β : Type u_3) [SDiff α] [SDiff β] :
SDiff (α × β)
Equations
instance Prod.instHasCompl (α : Type u_2) (β : Type u_3) [HasCompl α] [HasCompl β] :
HasCompl (α × β)
Equations
@[simp]
theorem fst_himp {α : Type u_2} {β : Type u_3} [HImp α] [HImp β] (a : α × β) (b : α × β) :
(a b).1 = a.1 b.1
@[simp]
theorem snd_himp {α : Type u_2} {β : Type u_3} [HImp α] [HImp β] (a : α × β) (b : α × β) :
(a b).2 = a.2 b.2
@[simp]
theorem fst_hnot {α : Type u_2} {β : Type u_3} [HNot α] [HNot β] (a : α × β) :
(a).1 = a.1
@[simp]
theorem snd_hnot {α : Type u_2} {β : Type u_3} [HNot α] [HNot β] (a : α × β) :
(a).2 = a.2
@[simp]
theorem fst_sdiff {α : Type u_2} {β : Type u_3} [SDiff α] [SDiff β] (a : α × β) (b : α × β) :
(a \ b).1 = a.1 \ b.1
@[simp]
theorem snd_sdiff {α : Type u_2} {β : Type u_3} [SDiff α] [SDiff β] (a : α × β) (b : α × β) :
(a \ b).2 = a.2 \ b.2
@[simp]
theorem fst_compl {α : Type u_2} {β : Type u_3} [HasCompl α] [HasCompl β] (a : α × β) :
a.1 = a.1
@[simp]
theorem snd_compl {α : Type u_2} {β : Type u_3} [HasCompl α] [HasCompl β] (a : α × β) :
a.2 = a.2
instance Pi.instHImpForall {ι : Type u_1} {π : ιType u_4} [(i : ι) → HImp (π i)] :
HImp ((i : ι) → π i)
Equations
  • Pi.instHImpForall = { himp := fun (a b : (i : ι) → π i) (i : ι) => a i b i }
instance Pi.instHNotForall {ι : Type u_1} {π : ιType u_4} [(i : ι) → HNot (π i)] :
HNot ((i : ι) → π i)
Equations
  • Pi.instHNotForall = { hnot := fun (a : (i : ι) → π i) (i : ι) => a i }
theorem Pi.himp_def {ι : Type u_1} {π : ιType u_4} [(i : ι) → HImp (π i)] (a : (i : ι) → π i) (b : (i : ι) → π i) :
a b = fun (i : ι) => a i b i
theorem Pi.hnot_def {ι : Type u_1} {π : ιType u_4} [(i : ι) → HNot (π i)] (a : (i : ι) → π i) :
a = fun (i : ι) => a i
@[simp]
theorem Pi.himp_apply {ι : Type u_1} {π : ιType u_4} [(i : ι) → HImp (π i)] (a : (i : ι) → π i) (b : (i : ι) → π i) (i : ι) :
(a b) i = a i b i
@[simp]
theorem Pi.hnot_apply {ι : Type u_1} {π : ιType u_4} [(i : ι) → HNot (π i)] (a : (i : ι) → π i) (i : ι) :
(a) i = a i
class GeneralizedHeytingAlgebra (α : Type u_4) extends Lattice , OrderTop , HImp :
Type u_4

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

This generalizes HeytingAlgebra by not requiring a bottom element.

  • sup : ααα
  • le : ααProp
  • lt : ααProp
  • le_refl : ∀ (a : α), a a
  • le_trans : ∀ (a b c : α), a bb ca c
  • lt_iff_le_not_le : ∀ (a b : α), a < b a b ¬b a
  • le_antisymm : ∀ (a b : α), a bb aa = b
  • le_sup_left : ∀ (a b : α), a a b
  • le_sup_right : ∀ (a b : α), b a b
  • sup_le : ∀ (a b c : α), a cb ca b c
  • inf : ααα
  • inf_le_left : ∀ (a b : α), a b a
  • inf_le_right : ∀ (a b : α), a b b
  • le_inf : ∀ (a b c : α), a ba ca b c
  • top : α
  • le_top : ∀ (a : α), a
  • himp : ααα
  • le_himp_iff : ∀ (a b c : α), a b c a b c

    (a ⇨ ·) is right adjoint to (a ⊓ ·)

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

    (a ⇨ ·) is right adjoint to (a ⊓ ·)

    class GeneralizedCoheytingAlgebra (α : Type u_4) extends Lattice , OrderBot , SDiff :
    Type u_4

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

    This generalizes CoheytingAlgebra by not requiring a top element.

    • sup : ααα
    • le : ααProp
    • lt : ααProp
    • le_refl : ∀ (a : α), a a
    • le_trans : ∀ (a b c : α), a bb ca c
    • lt_iff_le_not_le : ∀ (a b : α), a < b a b ¬b a
    • le_antisymm : ∀ (a b : α), a bb aa = b
    • le_sup_left : ∀ (a b : α), a a b
    • le_sup_right : ∀ (a b : α), b a b
    • sup_le : ∀ (a b c : α), a cb ca b c
    • inf : ααα
    • inf_le_left : ∀ (a b : α), a b a
    • inf_le_right : ∀ (a b : α), a b b
    • le_inf : ∀ (a b c : α), a ba ca b c
    • bot : α
    • bot_le : ∀ (a : α), a
    • sdiff : ααα
    • sdiff_le_iff : ∀ (a b c : α), a \ b c a b c

      (· \ a) is right adjoint to (· ⊔ a)

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

      (· \ a) is right adjoint to (· ⊔ a)

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

      • sup : ααα
      • le : ααProp
      • lt : ααProp
      • le_refl : ∀ (a : α), a a
      • le_trans : ∀ (a b c : α), a bb ca c
      • lt_iff_le_not_le : ∀ (a b : α), a < b a b ¬b a
      • le_antisymm : ∀ (a b : α), a bb aa = b
      • le_sup_left : ∀ (a b : α), a a b
      • le_sup_right : ∀ (a b : α), b a b
      • sup_le : ∀ (a b c : α), a cb ca b c
      • inf : ααα
      • inf_le_left : ∀ (a b : α), a b a
      • inf_le_right : ∀ (a b : α), a b b
      • le_inf : ∀ (a b c : α), a ba ca b c
      • top : α
      • le_top : ∀ (a : α), a
      • himp : ααα
      • le_himp_iff : ∀ (a b c : α), a b c a b c
      • bot : α
      • bot_le : ∀ (a : α), a
      • compl : αα
      • himp_bot : ∀ (a : α), a = a

        aᶜ is defined as a ⇨ ⊥

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

        aᶜ is defined as a ⇨ ⊥

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

        • sup : ααα
        • le : ααProp
        • lt : ααProp
        • le_refl : ∀ (a : α), a a
        • le_trans : ∀ (a b c : α), a bb ca c
        • lt_iff_le_not_le : ∀ (a b : α), a < b a b ¬b a
        • le_antisymm : ∀ (a b : α), a bb aa = b
        • le_sup_left : ∀ (a b : α), a a b
        • le_sup_right : ∀ (a b : α), b a b
        • sup_le : ∀ (a b c : α), a cb ca b c
        • inf : ααα
        • inf_le_left : ∀ (a b : α), a b a
        • inf_le_right : ∀ (a b : α), a b b
        • le_inf : ∀ (a b c : α), a ba ca b c
        • bot : α
        • bot_le : ∀ (a : α), a
        • sdiff : ααα
        • sdiff_le_iff : ∀ (a b c : α), a \ b c a b c
        • top : α
        • le_top : ∀ (a : α), a
        • hnot : αα
        • top_sdiff : ∀ (a : α), \ a = a

          ⊤ \ a is ¬a

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

          ⊤ \ a is ¬a

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

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

          • sup : ααα
          • le : ααProp
          • lt : ααProp
          • le_refl : ∀ (a : α), a a
          • le_trans : ∀ (a b c : α), a bb ca c
          • lt_iff_le_not_le : ∀ (a b : α), a < b a b ¬b a
          • le_antisymm : ∀ (a b : α), a bb aa = b
          • le_sup_left : ∀ (a b : α), a a b
          • le_sup_right : ∀ (a b : α), b a b
          • sup_le : ∀ (a b c : α), a cb ca b c
          • inf : ααα
          • inf_le_left : ∀ (a b : α), a b a
          • inf_le_right : ∀ (a b : α), a b b
          • le_inf : ∀ (a b c : α), a ba ca b c
          • top : α
          • le_top : ∀ (a : α), a
          • himp : ααα
          • le_himp_iff : ∀ (a b c : α), a b c a b c
          • bot : α
          • bot_le : ∀ (a : α), a
          • compl : αα
          • himp_bot : ∀ (a : α), a = a
          • sdiff : ααα
          • hnot : αα
          • sdiff_le_iff : ∀ (a b c : α), a \ b c a b c

            (· \ a) is right adjoint to (· ⊔ a)

          • top_sdiff : ∀ (a : α), \ a = a

            ⊤ \ a is ¬a

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

            (· \ a) is right adjoint to (· ⊔ a)

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

            ⊤ \ a is ¬a

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

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

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

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

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

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

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

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

                  Equations
                  Instances For

                    In this section, we'll give interpretations of these results in the Heyting algebra model of intuitionistic logic,- where can be interpreted as "validates", as "implies", as "and", as "or", as "false" and as "true". Note that we confuse and because those are the same in this logic.

                    See also Prop.heytingAlgebra.

                    @[simp]
                    theorem le_himp_iff {α : Type u_2} [GeneralizedHeytingAlgebra α] {a : α} {b : α} {c : α} :
                    a b c a b c

                    p → q → r ↔ p ∧ q → r

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

                    p → q → r ↔ q ∧ p → r

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

                    p → q → r ↔ q → p → r

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

                    p → q → p

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

                    p → p → q ↔ p → q

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

                    p → p

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

                    (p → q) ∧ p → q

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

                    p ∧ (p → q) → q

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

                    p ∧ (p → q) ↔ p ∧ q

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

                    (p → q) ∧ p ↔ q ∧ p

                    @[simp]
                    theorem himp_eq_top_iff {α : Type u_2} [GeneralizedHeytingAlgebra α] {a : α} {b : α} :
                    a b = a b

                    The deduction theorem in the Heyting algebra model of intuitionistic logic: an implication holds iff the conclusion follows from the hypothesis.

                    @[simp]
                    theorem himp_top {α : Type u_2} [GeneralizedHeytingAlgebra α] {a : α} :

                    p → true, true → p ↔ p

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

                    p → q → r ↔ p ∧ q → r

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

                    (q → r) → (p → q) → q → r

                    @[simp]
                    theorem himp_inf_himp_inf_le {α : Type u_2} [GeneralizedHeytingAlgebra α] {a : α} {b : α} {c : α} :
                    (b c) (a b) a c
                    theorem himp_left_comm {α : Type u_2} [GeneralizedHeytingAlgebra α] (a : α) (b : α) (c : α) :
                    a b c = b a c

                    p → q → r ↔ q → p → r

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

                    See himp_le for a stronger version in Boolean algebras.

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

                    Alias of sdiff_sup_self.

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

                    Alias of sup_sdiff_self.

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

                    See le_sdiff for a stronger version in generalised Boolean algebras.

                    theorem sdiff_sdiff_le {α : Type u_2} [GeneralizedCoheytingAlgebra α] {a : α} {b : α} :
                    a \ (a \ b) b
                    @[simp]
                    theorem sdiff_eq_sdiff_iff {α : Type u_2} [GeneralizedCoheytingAlgebra α] {a : α} {b : α} :
                    a \ b = b \ a a = b
                    theorem sdiff_ne_sdiff_iff {α : Type u_2} [GeneralizedCoheytingAlgebra α] {a : α} {b : α} :
                    a \ b b \ a a b
                    theorem sdiff_triangle {α : Type u_2} [GeneralizedCoheytingAlgebra α] (a : α) (b : α) (c : α) :
                    a \ c a \ b b \ c
                    theorem sdiff_sup_sdiff_cancel {α : Type u_2} [GeneralizedCoheytingAlgebra α] {a : α} {b : α} {c : α} (hba : b a) (hcb : c b) :
                    a \ b b \ c = a \ c
                    theorem sdiff_le_sdiff_of_sup_le_sup_left {α : Type u_2} [GeneralizedCoheytingAlgebra α] {a : α} {b : α} {c : α} (h : c a c b) :
                    a \ c b \ c
                    theorem sdiff_le_sdiff_of_sup_le_sup_right {α : Type u_2} [GeneralizedCoheytingAlgebra α] {a : α} {b : α} {c : α} (h : a c b c) :
                    a \ c b \ c
                    @[simp]
                    theorem inf_sdiff_sup_left {α : Type u_2} [GeneralizedCoheytingAlgebra α] {a : α} {b : α} {c : α} :
                    a \ c (a b) = a \ c
                    @[simp]
                    theorem inf_sdiff_sup_right {α : Type u_2} [GeneralizedCoheytingAlgebra α] {a : α} {b : α} {c : α} :
                    a \ c (b a) = a \ c
                    @[instance 100]
                    Equations
                    instance Pi.instGeneralizedCoheytingAlgebra {ι : Type u_1} {α : ιType u_4} [(i : ι) → GeneralizedCoheytingAlgebra (α i)] :
                    GeneralizedCoheytingAlgebra ((i : ι) → α i)
                    Equations
                    @[simp]
                    theorem himp_bot {α : Type u_2} [HeytingAlgebra α] (a : α) :
                    @[simp]
                    theorem bot_himp {α : Type u_2} [HeytingAlgebra α] (a : α) :
                    theorem compl_sup_distrib {α : Type u_2} [HeytingAlgebra α] (a : α) (b : α) :
                    (a b) = a b
                    @[simp]
                    theorem compl_sup {α : Type u_2} [HeytingAlgebra α] {a : α} {b : α} :
                    (a b) = a b
                    theorem compl_le_himp {α : Type u_2} [HeytingAlgebra α] {a : α} {b : α} :
                    a a b
                    theorem compl_sup_le_himp {α : Type u_2} [HeytingAlgebra α] {a : α} {b : α} :
                    a b a b
                    theorem sup_compl_le_himp {α : Type u_2} [HeytingAlgebra α] {a : α} {b : α} :
                    b a a b
                    @[simp]
                    theorem himp_compl {α : Type u_2} [HeytingAlgebra α] (a : α) :
                    a a = a
                    theorem himp_compl_comm {α : Type u_2} [HeytingAlgebra α] (a : α) (b : α) :
                    a b = b a
                    theorem le_compl_iff_disjoint_right {α : Type u_2} [HeytingAlgebra α] {a : α} {b : α} :
                    theorem le_compl_iff_disjoint_left {α : Type u_2} [HeytingAlgebra α] {a : α} {b : α} :
                    theorem le_compl_comm {α : Type u_2} [HeytingAlgebra α] {a : α} {b : α} :
                    a b b a
                    theorem Disjoint.le_compl_right {α : Type u_2} [HeytingAlgebra α] {a : α} {b : α} :
                    Disjoint a ba b

                    Alias of the reverse direction of le_compl_iff_disjoint_right.

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

                    Alias of the reverse direction of le_compl_iff_disjoint_left.

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

                    Alias of le_compl_comm.

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

                    Alias of the forward direction of le_compl_comm.

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

                    Alias of the reverse direction of hnot_le_iff_codisjoint_right.

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

                    Alias of the reverse direction of hnot_le_iff_codisjoint_left.

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

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

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

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

                      Pullback a GeneralizedHeytingAlgebra along an injection.

                      Equations
                      Instances For
                        @[reducible, inline]
                        abbrev Function.Injective.generalizedCoheytingAlgebra {α : Type u_2} {β : Type u_3} [Sup α] [Inf α] [Bot α] [SDiff α] [GeneralizedCoheytingAlgebra β] (f : αβ) (hf : Function.Injective f) (map_sup : ∀ (a b : α), f (a b) = f a f b) (map_inf : ∀ (a b : α), f (a b) = f a f b) (map_bot : f = ) (map_sdiff : ∀ (a b : α), f (a \ b) = f a \ f b) :

                        Pullback a GeneralizedCoheytingAlgebra along an injection.

                        Equations
                        Instances For
                          @[reducible, inline]
                          abbrev Function.Injective.heytingAlgebra {α : Type u_2} {β : Type u_3} [Sup α] [Inf α] [Top α] [Bot α] [HasCompl α] [HImp α] [HeytingAlgebra β] (f : αβ) (hf : Function.Injective f) (map_sup : ∀ (a b : α), f (a b) = f a f b) (map_inf : ∀ (a b : α), f (a b) = f a f b) (map_top : f = ) (map_bot : f = ) (map_compl : ∀ (a : α), f a = (f a)) (map_himp : ∀ (a b : α), f (a b) = f a f b) :

                          Pullback a HeytingAlgebra along an injection.

                          Equations
                          Instances For
                            @[reducible, inline]
                            abbrev Function.Injective.coheytingAlgebra {α : Type u_2} {β : Type u_3} [Sup α] [Inf α] [Top α] [Bot α] [HNot α] [SDiff α] [CoheytingAlgebra β] (f : αβ) (hf : Function.Injective f) (map_sup : ∀ (a b : α), f (a b) = f a f b) (map_inf : ∀ (a b : α), f (a b) = f a f b) (map_top : f = ) (map_bot : f = ) (map_hnot : ∀ (a : α), f (a) = f a) (map_sdiff : ∀ (a b : α), f (a \ b) = f a \ f b) :

                            Pullback a CoheytingAlgebra along an injection.

                            Equations
                            Instances For
                              @[reducible, inline]
                              abbrev Function.Injective.biheytingAlgebra {α : Type u_2} {β : Type u_3} [Sup α] [Inf α] [Top α] [Bot α] [HasCompl α] [HNot α] [HImp α] [SDiff α] [BiheytingAlgebra β] (f : αβ) (hf : Function.Injective f) (map_sup : ∀ (a b : α), f (a b) = f a f b) (map_inf : ∀ (a b : α), f (a b) = f a f b) (map_top : f = ) (map_bot : f = ) (map_compl : ∀ (a : α), f a = (f a)) (map_hnot : ∀ (a : α), f (a) = f a) (map_himp : ∀ (a b : α), f (a b) = f a f b) (map_sdiff : ∀ (a b : α), f (a \ b) = f a \ f b) :

                              Pullback a BiheytingAlgebra along an injection.

                              Equations
                              Instances For
                                @[simp]
                                @[simp]
                                @[simp]
                                @[simp]