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 #

Notation #

References #

Tags #

Heyting, Brouwer, algebra, implication, negation, intuitionistic

Notation #

class HImp (α : Type u_4) :
Type u_4
  • himp : ααα

    Heyting implication

Syntax typeclass for Heyting implication .

Instances
    class HNot (α : Type u_4) :
    Type u_4
    • hnot : αα

      Heyting negation

    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

      Heyting implication

      Instances For

        Heyting negation

        Instances For
          instance Prod.himp (α : Type u_2) (β : Type u_3) [HImp α] [HImp β] :
          HImp (α × β)
          instance Prod.hnot (α : Type u_2) (β : Type u_3) [HNot α] [HNot β] :
          HNot (α × β)
          instance Prod.sdiff (α : Type u_2) (β : Type u_3) [SDiff α] [SDiff β] :
          SDiff (α × β)
          instance Prod.hasCompl (α : Type u_2) (β : Type u_3) [HasCompl α] [HasCompl β] :
          HasCompl (α × β)
          @[simp]
          theorem fst_himp {α : Type u_2} {β : Type u_3} [HImp α] [HImp β] (a : α × β) (b : α × β) :
          (a b).fst = a.fst b.fst
          @[simp]
          theorem snd_himp {α : Type u_2} {β : Type u_3} [HImp α] [HImp β] (a : α × β) (b : α × β) :
          (a b).snd = a.snd b.snd
          @[simp]
          theorem fst_hnot {α : Type u_2} {β : Type u_3} [HNot α] [HNot β] (a : α × β) :
          (a).fst = a.fst
          @[simp]
          theorem snd_hnot {α : Type u_2} {β : Type u_3} [HNot α] [HNot β] (a : α × β) :
          (a).snd = a.snd
          @[simp]
          theorem fst_sdiff {α : Type u_2} {β : Type u_3} [SDiff α] [SDiff β] (a : α × β) (b : α × β) :
          (a \ b).fst = a.fst \ b.fst
          @[simp]
          theorem snd_sdiff {α : Type u_2} {β : Type u_3} [SDiff α] [SDiff β] (a : α × β) (b : α × β) :
          (a \ b).snd = a.snd \ b.snd
          @[simp]
          theorem fst_compl {α : Type u_2} {β : Type u_3} [HasCompl α] [HasCompl β] (a : α × β) :
          a.fst = a.fst
          @[simp]
          theorem snd_compl {α : Type u_2} {β : Type u_3} [HasCompl α] [HasCompl β] (a : α × β) :
          a.snd = a.snd
          instance Pi.instHImpForAll {ι : Type u_1} {π : ιType u_4} [(i : ι) → HImp (π i)] :
          HImp ((i : ι) → π i)
          instance Pi.instHNotForAll {ι : Type u_1} {π : ιType u_4} [(i : ι) → HNot (π i)] :
          HNot ((i : ι) → π 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 : ι) :
          (((i : ι) → π i) Pi.instHImpForAll) 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 : ι) :
          (((i : ι) → π i)) Pi.instHNotForAll a i = a i
          class GeneralizedHeytingAlgebra (α : Type u_4) extends Lattice , Top , HImp :
          Type u_4
          • 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 : α
          • himp : ααα
          • le_top : ∀ (a : α), a

            is a greatest element

          • le_himp_iff : ∀ (a b c : α), a b c a b c

            a ⇨ is right adjoint to a ⊓

          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_4) extends Lattice , Bot , SDiff :
            Type u_4
            • 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 : α
            • sdiff : ααα
            • bot_le : ∀ (a : α), a

              is a least element

            • sdiff_le_iff : ∀ (a b c : α), a \ b c a b c

              \ a is right adjoint to ⊔ a

            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.

            Instances
              class HeytingAlgebra (α : Type u_4) extends GeneralizedHeytingAlgebra , Bot , HasCompl :
              Type u_4
              • 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 : α
              • himp : ααα
              • le_top : ∀ (a : α), a
              • le_himp_iff : ∀ (a b c : α), a b c a b c
              • bot : α
              • compl : αα
              • bot_le : ∀ (a : α), a

                is a least element

              • himp_bot : ∀ (a : α), a = a

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

              Instances
                class CoheytingAlgebra (α : Type u_4) extends GeneralizedCoheytingAlgebra , Top , HNot :
                Type u_4
                • 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 : α
                • sdiff : ααα
                • bot_le : ∀ (a : α), a
                • sdiff_le_iff : ∀ (a b c : α), a \ b c a b c
                • top : α
                • hnot : αα
                • le_top : ∀ (a : α), a

                  is a greatest element

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

                  ⊤ \ a is ¬a

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

                Instances
                  class BiheytingAlgebra (α : Type u_4) extends HeytingAlgebra , SDiff , HNot :
                  Type u_4
                  • 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 : α
                  • himp : ααα
                  • le_top : ∀ (a : α), a
                  • le_himp_iff : ∀ (a b c : α), a b c a b c
                  • bot : α
                  • compl : αα
                  • bot_le : ∀ (a : α), a
                  • 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

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

                  Instances
                    @[reducible]
                    def 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.

                    Instances For
                      @[reducible]
                      def 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.

                      Instances For
                        @[reducible]
                        def 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.

                        Instances For
                          @[reducible]
                          def 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.

                          Instances For
                            @[simp]
                            theorem le_himp_iff {α : Type u_2} [GeneralizedHeytingAlgebra α] {a : α} {b : α} {c : α} :
                            a b c a b c
                            theorem le_himp_iff' {α : Type u_2} [GeneralizedHeytingAlgebra α] {a : α} {b : α} {c : α} :
                            a b c b a c
                            theorem le_himp_comm {α : Type u_2} [GeneralizedHeytingAlgebra α] {a : α} {b : α} {c : α} :
                            a b c b a c
                            theorem le_himp {α : Type u_2} [GeneralizedHeytingAlgebra α] {a : α} {b : α} :
                            a b a
                            theorem le_himp_iff_left {α : Type u_2} [GeneralizedHeytingAlgebra α] {a : α} {b : α} :
                            a a b a b
                            @[simp]
                            theorem himp_self {α : Type u_2} [GeneralizedHeytingAlgebra α] {a : α} :
                            a a =
                            theorem himp_inf_le {α : Type u_2} [GeneralizedHeytingAlgebra α] {a : α} {b : α} :
                            (a b) a b
                            theorem inf_himp_le {α : Type u_2} [GeneralizedHeytingAlgebra α] {a : α} {b : α} :
                            a (a b) b
                            @[simp]
                            theorem inf_himp {α : Type u_2} [GeneralizedHeytingAlgebra α] (a : α) (b : α) :
                            a (a b) = a b
                            @[simp]
                            theorem himp_inf_self {α : Type u_2} [GeneralizedHeytingAlgebra α] (a : α) (b : α) :
                            (a b) a = b a
                            @[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 : α} :
                            @[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
                            theorem himp_le_himp_himp_himp {α : Type u_2} [GeneralizedHeytingAlgebra α] {a : α} {b : α} {c : α} :
                            b c (a b) a c
                            @[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
                            @[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
                            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 Pi.generalizedHeytingAlgebra {ι : Type u_1} {α : ιType u_4} [(i : ι) → GeneralizedHeytingAlgebra (α i)] :
                            GeneralizedHeytingAlgebra ((i : ι) → α i)
                            @[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
                            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 Pi.generalizedCoheytingAlgebra {ι : Type u_1} {α : ιType u_4} [(i : ι) → GeneralizedCoheytingAlgebra (α i)] :
                            GeneralizedCoheytingAlgebra ((i : ι) → α i)
                            @[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 : α) :
                            @[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.heytingAlgebra {α : Type u_2} {β : Type u_3} [HeytingAlgebra α] [HeytingAlgebra β] :
                            instance Pi.heytingAlgebra {ι : Type u_1} {α : ιType u_4} [(i : ι) → HeytingAlgebra (α i)] :
                            HeytingAlgebra ((i : ι) → α i)
                            @[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
                            @[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 : α) :
                            @[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 Pi.coheytingAlgebra {ι : Type u_1} {α : ιType u_4} [(i : ι) → CoheytingAlgebra (α i)] :
                            CoheytingAlgebra ((i : ι) → α i)
                            theorem compl_le_hnot {α : Type u_2} [BiheytingAlgebra α] {a : α} :

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

                            @[simp]
                            theorem himp_iff_imp (p : Prop) (q : Prop) :
                            p q pq
                            @[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.
                            Instances For
                              @[reducible]
                              def 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.

                              Instances For
                                @[reducible]
                                def 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.

                                Instances For
                                  @[reducible]
                                  def 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.

                                  Instances For
                                    @[reducible]
                                    def 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.

                                    Instances For
                                      @[reducible]
                                      def 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.

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