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 #

Notation #

References #

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
      instance Prod.himp (α : Type u_1) (β : Type u_2) [inst : HImp α] [inst : HImp β] :
      HImp (α × β)
      Equations
      instance Prod.hnot (α : Type u_1) (β : Type u_2) [inst : HNot α] [inst : HNot β] :
      HNot (α × β)
      Equations
      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
      @[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
                Equations
                • GeneralizedHeytingAlgebra.toOrderTop = let src := inst; OrderTop.mk (_ : ∀ (a : α), a )
                Equations
                • GeneralizedCoheytingAlgebra.toOrderBot = let src := inst; OrderBot.mk (_ : ∀ (a : α), a)
                Equations
                • HeytingAlgebra.toBoundedOrder = BoundedOrder.mk
                Equations
                • CoheytingAlgebra.toBoundedOrder = let src := inst; BoundedOrder.mk
                Equations
                def HeytingAlgebra.ofHImp {α : Type u_1} [inst : DistribLattice α] [inst : 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
                def HeytingAlgebra.ofCompl {α : Type u_1} [inst : DistribLattice α] [inst : 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
                def CoheytingAlgebra.ofSDiff {α : Type u_1} [inst : DistribLattice α] [inst : 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
                def CoheytingAlgebra.ofHNot {α : Type u_1} [inst : DistribLattice α] [inst : 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
                @[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 : α} :
                a 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 : α} :
                @[simp]
                theorem top_himp {α : Type u_1} [inst : GeneralizedHeytingAlgebra α] {a : α} :
                a = 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
                Equations
                Equations
                • One or more equations did not get rendered due to their size.
                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
                Equations
                Equations
                • One or more equations did not get rendered due to their size.
                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 : α) :
                @[simp]
                theorem bot_himp {α : Type u_1} [inst : HeytingAlgebra α] (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 : α} :
                theorem le_compl_iff_disjoint_left {α : Type u_1} [inst : HeytingAlgebra α] {a : α} {b : α} :
                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 ba 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 aa 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 bb a

                Alias of the forward direction of le_compl_comm.

                theorem disjoint_compl_left {α : Type u_1} [inst : HeytingAlgebra α] {a : α} :
                theorem disjoint_compl_right {α : Type u_1} [inst : HeytingAlgebra α] {a : α} :
                theorem LE.le.disjoint_compl_left {α : Type u_1} [inst : HeytingAlgebra α] {a : α} {b : α} (h : b a) :
                theorem LE.le.disjoint_compl_right {α : Type u_1} [inst : HeytingAlgebra α] {a : α} {b : α} (h : 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 : α) :
                @[simp]
                theorem compl_inf_self {α : Type u_1} [inst : HeytingAlgebra α] (a : α) :
                theorem inf_compl_eq_bot {α : Type u_1} [inst : HeytingAlgebra α] {a : α} :
                theorem compl_inf_eq_bot {α : Type u_1} [inst : HeytingAlgebra α] {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 α] :
                Antitone compl
                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 : α) :
                @[simp]
                theorem disjoint_compl_compl_left_iff {α : Type u_1} [inst : HeytingAlgebra α] {a : α} {b : α} :
                @[simp]
                theorem disjoint_compl_compl_right_iff {α : Type u_1} [inst : HeytingAlgebra α] {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 : α) :
                theorem compl_compl_himp_distrib {α : Type u_1} [inst : HeytingAlgebra α] (a : α) (b : α) :
                Equations
                @[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 β] :
                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 : α) :
                \ a = 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
                Equations
                @[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 : α} :
                theorem hnot_le_iff_codisjoint_left {α : Type u_1} [inst : CoheytingAlgebra α] {a : α} {b : α} :
                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 ba 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 aa b

                Alias of the reverse direction of hnot_le_iff_codisjoint_left.

                theorem codisjoint_hnot_right {α : Type u_1} [inst : CoheytingAlgebra α] {a : α} :
                theorem codisjoint_hnot_left {α : Type u_1} [inst : CoheytingAlgebra α] {a : α} :
                theorem LE.le.codisjoint_hnot_left {α : Type u_1} [inst : CoheytingAlgebra α] {a : α} {b : α} (h : a b) :
                theorem LE.le.codisjoint_hnot_right {α : Type u_1} [inst : CoheytingAlgebra α] {a : α} {b : α} (h : b a) :
                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 : α) :
                @[simp]
                theorem hnot_sup_self {α : Type u_1} [inst : CoheytingAlgebra α] (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 : α) :
                @[simp]
                theorem codisjoint_hnot_hnot_left_iff {α : Type u_1} [inst : CoheytingAlgebra α] {a : α} {b : α} :
                @[simp]
                theorem codisjoint_hnot_hnot_right_iff {α : Type u_1} [inst : CoheytingAlgebra α] {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 : α) :
                theorem hnot_hnot_sdiff_distrib {α : Type u_1} [inst : CoheytingAlgebra α] (a : α) (b : α) :
                Equations
                @[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 β] :
                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 : α} :

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

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

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

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

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

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

                Pullback a BiheytingAlgebra along an injection.

                Equations
                • One or more equations did not get rendered due to their size.
                @[simp]
                theorem PUnit.sup_eq (a : PUnit) (b : PUnit) :
                @[simp]
                theorem PUnit.inf_eq (a : PUnit) (b : PUnit) :
                @[simp]
                @[simp]
                theorem PUnit.sdiff_eq (a : PUnit) (b : PUnit) :
                @[simp]
                @[simp]
                theorem PUnit.himp_eq (a : PUnit) (b : PUnit) :