Documentation

Mathlib.Order.CompleteBooleanAlgebra

Frames, completely distributive lattices and complete Boolean algebras #

In this file we define and provide API for (co)frames, completely distributive lattices and complete Boolean algebras.

We distinguish two different distributivity properties:

  1. inf_iSup_eq : (a ⊓ ⨆ i, f i) = ⨆ i, a ⊓ f i (finite distributes over infinite ). This is required by Frame, CompleteDistribLattice, and CompleteBooleanAlgebra (Coframe, etc., require the dual property).
  2. iInf_iSup_eq : (⨅ i, ⨆ j, f i j) = ⨆ s, ⨅ i, f i (s i) (infinite distributes over infinite ). This stronger property is called "completely distributive", and is required by CompletelyDistribLattice and CompleteAtomicBooleanAlgebra.

Typeclasses #

A set of opens gives rise to a topological space precisely if it forms a frame. Such a frame is also completely distributive, but not all frames are. Filter is a coframe but not a completely distributive lattice.

References #

Structure containing the minimal axioms required to check that an order is a frame. Do NOT use, except for implementing Order.Frame via Order.Frame.ofMinimalAxioms.

This structure omits the himp, compl fields, which can be recovered using Order.Frame.ofMinimalAxioms.

  • 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
  • sSup : Set αα
  • le_sSup : ∀ (s : Set α), as, a sSup s
  • sSup_le : ∀ (s : Set α) (a : α), (∀ bs, b a)sSup s a
  • sInf : Set αα
  • sInf_le : ∀ (s : Set α), as, sInf s a
  • le_sInf : ∀ (s : Set α) (a : α), (∀ bs, a b)a sInf s
  • top : α
  • bot : α
  • le_top : ∀ (x : α), x
  • bot_le : ∀ (x : α), x
  • inf_sSup_le_iSup_inf : ∀ (a : α) (s : Set α), a sSup s bs, a b
Instances
    theorem Order.Frame.MinimalAxioms.inf_sSup_le_iSup_inf {α : Type u} [self : Order.Frame.MinimalAxioms α] (a : α) (s : Set α) :
    a sSup s bs, a b

    Structure containing the minimal axioms required to check that an order is a coframe. Do NOT use, except for implementing Order.Coframe via Order.Coframe.ofMinimalAxioms.

    This structure omits the sdiff, hnot fields, which can be recovered using Order.Coframe.ofMinimalAxioms.

    • 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
    • sSup : Set αα
    • le_sSup : ∀ (s : Set α), as, a sSup s
    • sSup_le : ∀ (s : Set α) (a : α), (∀ bs, b a)sSup s a
    • sInf : Set αα
    • sInf_le : ∀ (s : Set α), as, sInf s a
    • le_sInf : ∀ (s : Set α) (a : α), (∀ bs, a b)a sInf s
    • top : α
    • bot : α
    • le_top : ∀ (x : α), x
    • bot_le : ∀ (x : α), x
    • iInf_sup_le_sup_sInf : ∀ (a : α) (s : Set α), bs, a b a sInf s
    Instances
      theorem Order.Coframe.MinimalAxioms.iInf_sup_le_sup_sInf {α : Type u} [self : Order.Coframe.MinimalAxioms α] (a : α) (s : Set α) :
      bs, a b a sInf s
      class Order.Frame (α : Type u_1) extends CompleteLattice , HImp , HasCompl :
      Type u_1

      A frame, aka complete Heyting algebra, is a complete lattice whose distributes over .

      • 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
      • sSup : Set αα
      • le_sSup : ∀ (s : Set α), as, a sSup s
      • sSup_le : ∀ (s : Set α) (a : α), (∀ bs, b a)sSup s a
      • sInf : Set αα
      • sInf_le : ∀ (s : Set α), as, sInf s a
      • le_sInf : ∀ (s : Set α) (a : α), (∀ bs, a b)a sInf s
      • top : α
      • bot : α
      • le_top : ∀ (x : α), x
      • bot_le : ∀ (x : α), x
      • himp : ααα
      • le_himp_iff : ∀ (a b c : α), a b c a b c

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

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

        aᶜ is defined as a ⇨ ⊥

      • inf_sSup_le_iSup_inf : ∀ (a : α) (s : Set α), a sSup s bs, a b

        distributes over .

      Instances
        theorem Order.Frame.inf_sSup_le_iSup_inf {α : Type u_1} [self : Order.Frame α] (a : α) (s : Set α) :
        a sSup s bs, a b

        distributes over .

        class Order.Coframe (α : Type u_1) extends CompleteLattice , SDiff , HNot :
        Type u_1

        A coframe, aka complete Brouwer algebra or complete co-Heyting algebra, is a complete lattice whose distributes over .

        • 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
        • sSup : Set αα
        • le_sSup : ∀ (s : Set α), as, a sSup s
        • sSup_le : ∀ (s : Set α) (a : α), (∀ bs, b a)sSup s a
        • sInf : Set αα
        • sInf_le : ∀ (s : Set α), as, sInf s a
        • le_sInf : ∀ (s : Set α) (a : α), (∀ bs, a b)a sInf s
        • top : α
        • bot : α
        • le_top : ∀ (x : α), x
        • bot_le : ∀ (x : α), x
        • sdiff : ααα
        • sdiff_le_iff : ∀ (a b c : α), a \ b c a b c

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

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

          ⊤ \ a is ¬a

        • iInf_sup_le_sup_sInf : ∀ (a : α) (s : Set α), bs, a b a sInf s

          distributes over .

        Instances
          theorem Order.Coframe.iInf_sup_le_sup_sInf {α : Type u_1} [self : Order.Coframe α] (a : α) (s : Set α) :
          bs, a b a sInf s

          distributes over .

          Structure containing the minimal axioms required to check that an order is a complete distributive lattice. Do NOT use, except for implementing CompleteDistribLattice via CompleteDistribLattice.ofMinimalAxioms.

          This structure omits the himp, compl, sdiff, hnot fields, which can be recovered using CompleteDistribLattice.ofMinimalAxioms.

          • 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
          • sSup : Set αα
          • le_sSup : ∀ (s : Set α), as, a sSup s
          • sSup_le : ∀ (s : Set α) (a : α), (∀ bs, b a)sSup s a
          • sInf : Set αα
          • sInf_le : ∀ (s : Set α), as, sInf s a
          • le_sInf : ∀ (s : Set α) (a : α), (∀ bs, a b)a sInf s
          • top : α
          • bot : α
          • le_top : ∀ (x : α), x
          • bot_le : ∀ (x : α), x
          • inf_sSup_le_iSup_inf : ∀ (a : α) (s : Set α), a sSup s bs, a b
          • iInf_sup_le_sup_sInf : ∀ (a : α) (s : Set α), bs, a b a sInf s
          Instances For
            class CompleteDistribLattice (α : Type u_1) extends Order.Frame , SDiff , HNot :
            Type u_1

            A complete distributive lattice is a complete lattice whose and respectively distribute over and .

            • 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
            • sSup : Set αα
            • le_sSup : ∀ (s : Set α), as, a sSup s
            • sSup_le : ∀ (s : Set α) (a : α), (∀ bs, b a)sSup s a
            • sInf : Set αα
            • sInf_le : ∀ (s : Set α), as, sInf s a
            • le_sInf : ∀ (s : Set α) (a : α), (∀ bs, a b)a sInf s
            • top : α
            • bot : α
            • le_top : ∀ (x : α), x
            • bot_le : ∀ (x : α), x
            • himp : ααα
            • le_himp_iff : ∀ (a b c : α), a b c a b c
            • compl : αα
            • himp_bot : ∀ (a : α), a = a
            • inf_sSup_le_iSup_inf : ∀ (a : α) (s : Set α), a sSup s bs, a b
            • sdiff : ααα
            • sdiff_le_iff : ∀ (a b c : α), a \ b c a b c

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

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

              ⊤ \ a is ¬a

            • iInf_sup_le_sup_sInf : ∀ (a : α) (s : Set α), bs, a b a sInf s

              distributes over .

            Instances
              theorem CompleteDistribLattice.iInf_sup_le_sup_sInf {α : Type u_1} [self : CompleteDistribLattice α] (a : α) (s : Set α) :
              bs, a b a sInf s

              distributes over .

              Structure containing the minimal axioms required to check that an order is a completely distributive. Do NOT use, except for implementing CompletelyDistribLattice via CompletelyDistribLattice.ofMinimalAxioms.

              This structure omits the himp, compl, sdiff, hnot fields, which can be recovered using CompletelyDistribLattice.ofMinimalAxioms.

              • 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
              • sSup : Set αα
              • le_sSup : ∀ (s : Set α), as, a sSup s
              • sSup_le : ∀ (s : Set α) (a : α), (∀ bs, b a)sSup s a
              • sInf : Set αα
              • sInf_le : ∀ (s : Set α), as, sInf s a
              • le_sInf : ∀ (s : Set α) (a : α), (∀ bs, a b)a sInf s
              • top : α
              • bot : α
              • le_top : ∀ (x : α), x
              • bot_le : ∀ (x : α), x
              • iInf_iSup_eq : ∀ {ι : Type u} {κ : ιType u} (f : (a : ι) → κ aα), ⨅ (a : ι), ⨆ (b : κ a), f a b = ⨆ (g : (a : ι) → κ a), ⨅ (a : ι), f a (g a)
              Instances For
                theorem CompletelyDistribLattice.MinimalAxioms.iInf_iSup_eq {α : Type u} (self : CompletelyDistribLattice.MinimalAxioms α) {ι : Type u} {κ : ιType u} (f : (a : ι) → κ aα) :
                ⨅ (a : ι), ⨆ (b : κ a), f a b = ⨆ (g : (a : ι) → κ a), ⨅ (a : ι), f a (g a)

                A completely distributive lattice is a complete lattice whose and distribute over each other.

                • 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
                • sSup : Set αα
                • le_sSup : ∀ (s : Set α), as, a sSup s
                • sSup_le : ∀ (s : Set α) (a : α), (∀ bs, b a)sSup s a
                • sInf : Set αα
                • sInf_le : ∀ (s : Set α), as, sInf s a
                • le_sInf : ∀ (s : Set α) (a : α), (∀ bs, a b)a sInf s
                • top : α
                • bot : α
                • le_top : ∀ (x : α), x
                • bot_le : ∀ (x : α), x
                • himp : ααα
                • le_himp_iff : ∀ (a b c : α), a b c a b c

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

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

                  aᶜ is defined as 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

                • iInf_iSup_eq : ∀ {ι : Type u} {κ : ιType u} (f : (a : ι) → κ aα), ⨅ (a : ι), ⨆ (b : κ a), f a b = ⨆ (g : (a : ι) → κ a), ⨅ (a : ι), f a (g a)
                Instances
                  theorem CompletelyDistribLattice.iInf_iSup_eq {α : Type u} [self : CompletelyDistribLattice α] {ι : Type u} {κ : ιType u} (f : (a : ι) → κ aα) :
                  ⨅ (a : ι), ⨆ (b : κ a), f a b = ⨆ (g : (a : ι) → κ a), ⨅ (a : ι), f a (g a)
                  theorem le_iInf_iSup {α : Type u} {ι : Sort w} {κ : ιSort w'} [CompleteLattice α] {f : (a : ι) → κ aα} :
                  ⨆ (g : (a : ι) → κ a), ⨅ (a : ι), f a (g a) ⨅ (a : ι), ⨆ (b : κ a), f a b
                  theorem iSup_iInf_le {α : Type u} {ι : Sort w} {κ : ιSort w'} [CompleteLattice α] {f : (a : ι) → κ aα} :
                  ⨆ (a : ι), ⨅ (b : κ a), f a b ⨅ (g : (a : ι) → κ a), ⨆ (a : ι), f a (g a)
                  theorem Order.Frame.MinimalAxioms.inf_sSup_eq {α : Type u} (minAx : Order.Frame.MinimalAxioms α) {s : Set α} {a : α} :
                  a sSup s = bs, a b
                  theorem Order.Frame.MinimalAxioms.sSup_inf_eq {α : Type u} (minAx : Order.Frame.MinimalAxioms α) {s : Set α} {b : α} :
                  sSup s b = as, a b
                  theorem Order.Frame.MinimalAxioms.iSup_inf_eq {α : Type u} {ι : Sort w} (minAx : Order.Frame.MinimalAxioms α) (f : ια) (a : α) :
                  (⨆ (i : ι), f i) a = ⨆ (i : ι), f i a
                  theorem Order.Frame.MinimalAxioms.inf_iSup_eq {α : Type u} {ι : Sort w} (minAx : Order.Frame.MinimalAxioms α) (a : α) (f : ια) :
                  a ⨆ (i : ι), f i = ⨆ (i : ι), a f i
                  theorem Order.Frame.MinimalAxioms.inf_iSup₂_eq {α : Type u} {ι : Sort w} {κ : ιSort w'} (minAx : Order.Frame.MinimalAxioms α) {f : (i : ι) → κ iα} (a : α) :
                  a ⨆ (i : ι), ⨆ (j : κ i), f i j = ⨆ (i : ι), ⨆ (j : κ i), a f i j

                  The Order.Frame.MinimalAxioms element corresponding to a frame.

                  Equations
                  Instances For
                    @[reducible, inline]

                    Construct a frame instance using the minimal amount of work needed.

                    This sets a ⇨ b := sSup {c | c ⊓ a ≤ b} and aᶜ := a ⇨ ⊥.

                    Equations
                    Instances For
                      theorem Order.Coframe.MinimalAxioms.sup_sInf_eq {α : Type u} (minAx : Order.Coframe.MinimalAxioms α) {s : Set α} {a : α} :
                      a sInf s = bs, a b
                      theorem Order.Coframe.MinimalAxioms.sInf_sup_eq {α : Type u} (minAx : Order.Coframe.MinimalAxioms α) {s : Set α} {b : α} :
                      sInf s b = as, a b
                      theorem Order.Coframe.MinimalAxioms.iInf_sup_eq {α : Type u} {ι : Sort w} (minAx : Order.Coframe.MinimalAxioms α) (f : ια) (a : α) :
                      (⨅ (i : ι), f i) a = ⨅ (i : ι), f i a
                      theorem Order.Coframe.MinimalAxioms.sup_iInf_eq {α : Type u} {ι : Sort w} (minAx : Order.Coframe.MinimalAxioms α) (a : α) (f : ια) :
                      a ⨅ (i : ι), f i = ⨅ (i : ι), a f i
                      theorem Order.Coframe.MinimalAxioms.sup_iInf₂_eq {α : Type u} {ι : Sort w} {κ : ιSort w'} (minAx : Order.Coframe.MinimalAxioms α) {f : (i : ι) → κ iα} (a : α) :
                      a ⨅ (i : ι), ⨅ (j : κ i), f i j = ⨅ (i : ι), ⨅ (j : κ i), a f i j

                      The Order.Coframe.MinimalAxioms element corresponding to a frame.

                      Equations
                      Instances For
                        @[reducible, inline]

                        Construct a coframe instance using the minimal amount of work needed.

                        This sets a \ b := sInf {c | a ≤ b ⊔ c} and ¬a := ⊤ \ a.

                        Equations
                        Instances For

                          The CompleteDistribLattice.MinimalAxioms element corresponding to a complete distrib lattice.

                          Equations
                          • CompleteDistribLattice.MinimalAxioms.of = { toCompleteLattice := Order.Frame.toCompleteLattice, inf_sSup_le_iSup_inf := , iInf_sup_le_sup_sInf := }
                          Instances For
                            @[reducible, inline]

                            Turn minimal axioms for CompleteDistribLattice into minimal axioms for Order.Frame.

                            Equations
                            • minAx.toFrame = minAx.toMinimalAxioms
                            Instances For
                              @[reducible, inline]

                              Turn minimal axioms for CompleteDistribLattice into minimal axioms for Order.Coframe.

                              Equations
                              Instances For
                                @[reducible, inline]

                                Construct a complete distrib lattice instance using the minimal amount of work needed.

                                This sets a ⇨ b := sSup {c | c ⊓ a ≤ b}, aᶜ := a ⇨ ⊥, a \ b := sInf {c | a ≤ b ⊔ c} and ¬a := ⊤ \ a.

                                Equations
                                Instances For
                                  theorem CompletelyDistribLattice.MinimalAxioms.iInf_iSup_eq' {α : Type u} {ι : Sort w} {κ : ιSort w'} (minAx : CompletelyDistribLattice.MinimalAxioms α) (f : (a : ι) → κ aα) :
                                  let x := minAx.toCompleteLattice; ⨅ (i : ι), ⨆ (j : κ i), f i j = ⨆ (g : (i : ι) → κ i), ⨅ (i : ι), f i (g i)
                                  theorem CompletelyDistribLattice.MinimalAxioms.iSup_iInf_eq {α : Type u} {ι : Sort w} {κ : ιSort w'} (minAx : CompletelyDistribLattice.MinimalAxioms α) (f : (i : ι) → κ iα) :
                                  let x := minAx.toCompleteLattice; ⨆ (i : ι), ⨅ (j : κ i), f i j = ⨅ (g : (i : ι) → κ i), ⨆ (i : ι), f i (g i)
                                  @[reducible, inline]

                                  Turn minimal axioms for CompletelyDistribLattice into minimal axioms for CompleteDistribLattice.

                                  Equations
                                  • minAx.toCompleteDistribLattice = { toCompleteLattice := minAx.toCompleteLattice, inf_sSup_le_iSup_inf := , iInf_sup_le_sup_sInf := }
                                  Instances For

                                    The CompletelyDistribLattice.MinimalAxioms element corresponding to a frame.

                                    Equations
                                    • CompletelyDistribLattice.MinimalAxioms.of = { toCompleteLattice := CompletelyDistribLattice.toCompleteLattice, iInf_iSup_eq := }
                                    Instances For
                                      @[reducible, inline]

                                      Construct a completely distributive lattice instance using the minimal amount of work needed.

                                      This sets a ⇨ b := sSup {c | c ⊓ a ≤ b}, aᶜ := a ⇨ ⊥, a \ b := sInf {c | a ≤ b ⊔ c} and ¬a := ⊤ \ a.

                                      Equations
                                      Instances For
                                        theorem iInf_iSup_eq {α : Type u} {ι : Sort w} {κ : ιSort w'} [CompletelyDistribLattice α] {f : (a : ι) → κ aα} :
                                        ⨅ (a : ι), ⨆ (b : κ a), f a b = ⨆ (g : (a : ι) → κ a), ⨅ (a : ι), f a (g a)
                                        theorem iSup_iInf_eq {α : Type u} {ι : Sort w} {κ : ιSort w'} [CompletelyDistribLattice α] {f : (a : ι) → κ aα} :
                                        ⨆ (a : ι), ⨅ (b : κ a), f a b = ⨅ (g : (a : ι) → κ a), ⨆ (a : ι), f a (g a)
                                        @[instance 100]
                                        Equations
                                        @[instance 100]
                                        Equations
                                        Equations
                                        theorem inf_sSup_eq {α : Type u} [Order.Frame α] {s : Set α} {a : α} :
                                        a sSup s = bs, a b
                                        theorem sSup_inf_eq {α : Type u} [Order.Frame α] {s : Set α} {b : α} :
                                        sSup s b = as, a b
                                        theorem iSup_inf_eq {α : Type u} {ι : Sort w} [Order.Frame α] (f : ια) (a : α) :
                                        (⨆ (i : ι), f i) a = ⨆ (i : ι), f i a
                                        theorem inf_iSup_eq {α : Type u} {ι : Sort w} [Order.Frame α] (a : α) (f : ια) :
                                        a ⨆ (i : ι), f i = ⨆ (i : ι), a f i
                                        theorem iSup₂_inf_eq {α : Type u} {ι : Sort w} {κ : ιSort w'} [Order.Frame α] {f : (i : ι) → κ iα} (a : α) :
                                        (⨆ (i : ι), ⨆ (j : κ i), f i j) a = ⨆ (i : ι), ⨆ (j : κ i), f i j a
                                        theorem inf_iSup₂_eq {α : Type u} {ι : Sort w} {κ : ιSort w'} [Order.Frame α] {f : (i : ι) → κ iα} (a : α) :
                                        a ⨆ (i : ι), ⨆ (j : κ i), f i j = ⨆ (i : ι), ⨆ (j : κ i), a f i j
                                        theorem iSup_inf_iSup {α : Type u} [Order.Frame α] {ι : Type u_1} {ι' : Type u_2} {f : ια} {g : ι'α} :
                                        (⨆ (i : ι), f i) ⨆ (j : ι'), g j = ⨆ (i : ι × ι'), f i.1 g i.2
                                        theorem biSup_inf_biSup {α : Type u} [Order.Frame α] {ι : Type u_1} {ι' : Type u_2} {f : ια} {g : ι'α} {s : Set ι} {t : Set ι'} :
                                        (⨆ is, f i) jt, g j = ps ×ˢ t, f p.1 g p.2
                                        theorem sSup_inf_sSup {α : Type u} [Order.Frame α] {s : Set α} {t : Set α} :
                                        sSup s sSup t = ps ×ˢ t, p.1 p.2
                                        theorem iSup_disjoint_iff {α : Type u} {ι : Sort w} [Order.Frame α] {a : α} {f : ια} :
                                        Disjoint (⨆ (i : ι), f i) a ∀ (i : ι), Disjoint (f i) a
                                        theorem disjoint_iSup_iff {α : Type u} {ι : Sort w} [Order.Frame α] {a : α} {f : ια} :
                                        Disjoint a (⨆ (i : ι), f i) ∀ (i : ι), Disjoint a (f i)
                                        theorem iSup₂_disjoint_iff {α : Type u} {ι : Sort w} {κ : ιSort w'} [Order.Frame α] {a : α} {f : (i : ι) → κ iα} :
                                        Disjoint (⨆ (i : ι), ⨆ (j : κ i), f i j) a ∀ (i : ι) (j : κ i), Disjoint (f i j) a
                                        theorem disjoint_iSup₂_iff {α : Type u} {ι : Sort w} {κ : ιSort w'} [Order.Frame α] {a : α} {f : (i : ι) → κ iα} :
                                        Disjoint a (⨆ (i : ι), ⨆ (j : κ i), f i j) ∀ (i : ι) (j : κ i), Disjoint a (f i j)
                                        theorem sSup_disjoint_iff {α : Type u} [Order.Frame α] {a : α} {s : Set α} :
                                        Disjoint (sSup s) a bs, Disjoint b a
                                        theorem disjoint_sSup_iff {α : Type u} [Order.Frame α] {a : α} {s : Set α} :
                                        Disjoint a (sSup s) bs, Disjoint a b
                                        theorem iSup_inf_of_monotone {α : Type u} [Order.Frame α] {ι : Type u_1} [Preorder ι] [IsDirected ι fun (x1 x2 : ι) => x1 x2] {f : ια} {g : ια} (hf : Monotone f) (hg : Monotone g) :
                                        ⨆ (i : ι), f i g i = (⨆ (i : ι), f i) ⨆ (i : ι), g i
                                        theorem iSup_inf_of_antitone {α : Type u} [Order.Frame α] {ι : Type u_1} [Preorder ι] [IsDirected ι (Function.swap fun (x1 x2 : ι) => x1 x2)] {f : ια} {g : ια} (hf : Antitone f) (hg : Antitone g) :
                                        ⨆ (i : ι), f i g i = (⨆ (i : ι), f i) ⨆ (i : ι), g i
                                        @[instance 100]
                                        Equations
                                        instance Prod.instFrame {α : Type u} {β : Type v} [Order.Frame α] [Order.Frame β] :
                                        Order.Frame (α × β)
                                        Equations
                                        instance Pi.instFrame {ι : Type u_1} {π : ιType u_2} [(i : ι) → Order.Frame (π i)] :
                                        Order.Frame ((i : ι) → π i)
                                        Equations
                                        Equations
                                        theorem sup_sInf_eq {α : Type u} [Order.Coframe α] {s : Set α} {a : α} :
                                        a sInf s = bs, a b
                                        theorem sInf_sup_eq {α : Type u} [Order.Coframe α] {s : Set α} {b : α} :
                                        sInf s b = as, a b
                                        theorem iInf_sup_eq {α : Type u} {ι : Sort w} [Order.Coframe α] (f : ια) (a : α) :
                                        (⨅ (i : ι), f i) a = ⨅ (i : ι), f i a
                                        theorem sup_iInf_eq {α : Type u} {ι : Sort w} [Order.Coframe α] (a : α) (f : ια) :
                                        a ⨅ (i : ι), f i = ⨅ (i : ι), a f i
                                        theorem iInf₂_sup_eq {α : Type u} {ι : Sort w} {κ : ιSort w'} [Order.Coframe α] {f : (i : ι) → κ iα} (a : α) :
                                        (⨅ (i : ι), ⨅ (j : κ i), f i j) a = ⨅ (i : ι), ⨅ (j : κ i), f i j a
                                        theorem sup_iInf₂_eq {α : Type u} {ι : Sort w} {κ : ιSort w'} [Order.Coframe α] {f : (i : ι) → κ iα} (a : α) :
                                        a ⨅ (i : ι), ⨅ (j : κ i), f i j = ⨅ (i : ι), ⨅ (j : κ i), a f i j
                                        theorem iInf_sup_iInf {α : Type u} [Order.Coframe α] {ι : Type u_1} {ι' : Type u_2} {f : ια} {g : ι'α} :
                                        (⨅ (i : ι), f i) ⨅ (i : ι'), g i = ⨅ (i : ι × ι'), f i.1 g i.2
                                        theorem biInf_sup_biInf {α : Type u} [Order.Coframe α] {ι : Type u_1} {ι' : Type u_2} {f : ια} {g : ι'α} {s : Set ι} {t : Set ι'} :
                                        (⨅ is, f i) jt, g j = ps ×ˢ t, f p.1 g p.2
                                        theorem sInf_sup_sInf {α : Type u} [Order.Coframe α] {s : Set α} {t : Set α} :
                                        sInf s sInf t = ps ×ˢ t, p.1 p.2
                                        theorem iInf_sup_of_monotone {α : Type u} [Order.Coframe α] {ι : Type u_1} [Preorder ι] [IsDirected ι (Function.swap fun (x1 x2 : ι) => x1 x2)] {f : ια} {g : ια} (hf : Monotone f) (hg : Monotone g) :
                                        ⨅ (i : ι), f i g i = (⨅ (i : ι), f i) ⨅ (i : ι), g i
                                        theorem iInf_sup_of_antitone {α : Type u} [Order.Coframe α] {ι : Type u_1} [Preorder ι] [IsDirected ι fun (x1 x2 : ι) => x1 x2] {f : ια} {g : ια} (hf : Antitone f) (hg : Antitone g) :
                                        ⨅ (i : ι), f i g i = (⨅ (i : ι), f i) ⨅ (i : ι), g i
                                        @[instance 100]
                                        Equations
                                        instance Prod.instCoframe {α : Type u} {β : Type v} [Order.Coframe α] [Order.Coframe β] :
                                        Equations
                                        instance Pi.instCoframe {ι : Type u_1} {π : ιType u_2} [(i : ι) → Order.Coframe (π i)] :
                                        Order.Coframe ((i : ι) → π i)
                                        Equations
                                        Equations
                                        Equations
                                        instance Pi.instCompleteDistribLattice {ι : Type u_1} {π : ιType u_2} [(i : ι) → CompleteDistribLattice (π i)] :
                                        CompleteDistribLattice ((i : ι) → π i)
                                        Equations
                                        Equations
                                        Equations
                                        instance Pi.instCompletelyDistribLattice {ι : Type u_1} {π : ιType u_2} [(i : ι) → CompletelyDistribLattice (π i)] :
                                        CompletelyDistribLattice ((i : ι) → π i)
                                        Equations
                                        class CompleteBooleanAlgebra (α : Type u_1) extends CompleteLattice , HasCompl , SDiff , HImp :
                                        Type u_1

                                        A complete Boolean algebra is a Boolean algebra that is also a complete distributive lattice.

                                        It is only completely distributive if it is also atomic.

                                        • 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
                                        • sSup : Set αα
                                        • le_sSup : ∀ (s : Set α), as, a sSup s
                                        • sSup_le : ∀ (s : Set α) (a : α), (∀ bs, b a)sSup s a
                                        • sInf : Set αα
                                        • sInf_le : ∀ (s : Set α), as, sInf s a
                                        • le_sInf : ∀ (s : Set α) (a : α), (∀ bs, a b)a sInf s
                                        • top : α
                                        • bot : α
                                        • le_top : ∀ (x : α), x
                                        • bot_le : ∀ (x : α), x
                                        • le_sup_inf : ∀ (x y z : α), (x y) (x z) x y z

                                          The infimum distributes over the supremum

                                        • compl : αα
                                        • sdiff : ααα
                                        • himp : ααα
                                        • inf_compl_le_bot : ∀ (x : α), x x

                                          The infimum of x and xᶜ is at most

                                        • top_le_sup_compl : ∀ (x : α), x x

                                          The supremum of x and xᶜ is at least

                                        • sdiff_eq : ∀ (x y : α), x \ y = x y

                                          x \ y is equal to x ⊓ yᶜ

                                        • himp_eq : ∀ (x y : α), x y = y x

                                          x ⇨ y is equal to y ⊔ xᶜ

                                        • inf_sSup_le_iSup_inf : ∀ (a : α) (s : Set α), a sSup s bs, a b

                                          distributes over .

                                        • iInf_sup_le_sup_sInf : ∀ (a : α) (s : Set α), bs, a b a sInf s

                                          distributes over .

                                        Instances
                                          theorem CompleteBooleanAlgebra.inf_sSup_le_iSup_inf {α : Type u_1} [self : CompleteBooleanAlgebra α] (a : α) (s : Set α) :
                                          a sSup s bs, a b

                                          distributes over .

                                          theorem CompleteBooleanAlgebra.iInf_sup_le_sup_sInf {α : Type u_1} [self : CompleteBooleanAlgebra α] (a : α) (s : Set α) :
                                          bs, a b a sInf s

                                          distributes over .

                                          @[instance 100]
                                          Equations
                                          Equations
                                          instance Pi.instCompleteBooleanAlgebra {ι : Type u_1} {π : ιType u_2} [(i : ι) → CompleteBooleanAlgebra (π i)] :
                                          CompleteBooleanAlgebra ((i : ι) → π i)
                                          Equations
                                          Equations
                                          theorem compl_iInf {α : Type u} {ι : Sort w} [CompleteBooleanAlgebra α] {f : ια} :
                                          (iInf f) = ⨆ (i : ι), (f i)
                                          theorem compl_iSup {α : Type u} {ι : Sort w} [CompleteBooleanAlgebra α] {f : ια} :
                                          (iSup f) = ⨅ (i : ι), (f i)
                                          theorem compl_sInf {α : Type u} [CompleteBooleanAlgebra α] {s : Set α} :
                                          (sInf s) = is, i
                                          theorem compl_sSup {α : Type u} [CompleteBooleanAlgebra α] {s : Set α} :
                                          (sSup s) = is, i
                                          theorem compl_sInf' {α : Type u} [CompleteBooleanAlgebra α] {s : Set α} :
                                          (sInf s) = sSup (compl '' s)
                                          theorem compl_sSup' {α : Type u} [CompleteBooleanAlgebra α] {s : Set α} :
                                          (sSup s) = sInf (compl '' s)
                                          theorem iSup_symmDiff_iSup_le {α : Type u} {ι : Sort w} [CompleteBooleanAlgebra α] {f : ια} {g : ια} :
                                          symmDiff (⨆ (i : ι), f i) (⨆ (i : ι), g i) ⨆ (i : ι), symmDiff (f i) (g i)

                                          The symmetric difference of two iSups is at most the iSup of the symmetric differences.

                                          theorem biSup_symmDiff_biSup_le {α : Type u} {ι : Sort w} [CompleteBooleanAlgebra α] {p : ιProp} {f : (i : ι) → p iα} {g : (i : ι) → p iα} :
                                          symmDiff (⨆ (i : ι), ⨆ (h : p i), f i h) (⨆ (i : ι), ⨆ (h : p i), g i h) ⨆ (i : ι), ⨆ (h : p i), symmDiff (f i h) (g i h)

                                          A biSup version of iSup_symmDiff_iSup_le.

                                          A complete atomic Boolean algebra is a complete Boolean algebra that is also completely distributive.

                                          We take iSup_iInf_eq as the definition here, and prove later on that this implies atomicity.

                                          • 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
                                          • sSup : Set αα
                                          • le_sSup : ∀ (s : Set α), as, a sSup s
                                          • sSup_le : ∀ (s : Set α) (a : α), (∀ bs, b a)sSup s a
                                          • sInf : Set αα
                                          • sInf_le : ∀ (s : Set α), as, sInf s a
                                          • le_sInf : ∀ (s : Set α) (a : α), (∀ bs, a b)a sInf s
                                          • top : α
                                          • bot : α
                                          • le_top : ∀ (x : α), x
                                          • bot_le : ∀ (x : α), x
                                          • le_sup_inf : ∀ (x y z : α), (x y) (x z) x y z

                                            The infimum distributes over the supremum

                                          • compl : αα
                                          • sdiff : ααα
                                          • himp : ααα
                                          • inf_compl_le_bot : ∀ (x : α), x x

                                            The infimum of x and xᶜ is at most

                                          • top_le_sup_compl : ∀ (x : α), x x

                                            The supremum of x and xᶜ is at least

                                          • sdiff_eq : ∀ (x y : α), x \ y = x y

                                            x \ y is equal to x ⊓ yᶜ

                                          • himp_eq : ∀ (x y : α), x y = y x

                                            x ⇨ y is equal to y ⊔ xᶜ

                                          • iInf_iSup_eq : ∀ {ι : Type u} {κ : ιType u} (f : (a : ι) → κ aα), ⨅ (a : ι), ⨆ (b : κ a), f a b = ⨆ (g : (a : ι) → κ a), ⨅ (a : ι), f a (g a)
                                          Instances
                                            theorem CompleteAtomicBooleanAlgebra.iInf_iSup_eq {α : Type u} [self : CompleteAtomicBooleanAlgebra α] {ι : Type u} {κ : ιType u} (f : (a : ι) → κ aα) :
                                            ⨅ (a : ι), ⨆ (b : κ a), f a b = ⨆ (g : (a : ι) → κ a), ⨅ (a : ι), f a (g a)
                                            @[instance 100]
                                            Equations
                                            @[instance 100]
                                            Equations
                                            Equations
                                            instance Pi.instCompleteAtomicBooleanAlgebra {ι : Type u_1} {π : ιType u_2} [(i : ι) → CompleteAtomicBooleanAlgebra (π i)] :
                                            CompleteAtomicBooleanAlgebra ((i : ι) → π i)
                                            Equations
                                            Equations
                                            @[reducible, inline]
                                            abbrev Function.Injective.frameMinimalAxioms {α : Type u} {β : Type v} [Sup α] [Inf α] [SupSet α] [InfSet α] [Top α] [Bot α] (minAx : Order.Frame.MinimalAxioms β) (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_sSup : ∀ (s : Set α), f (sSup s) = as, f a) (map_sInf : ∀ (s : Set α), f (sInf s) = as, f a) (map_top : f = ) (map_bot : f = ) :

                                            Pullback an Order.Frame.MinimalAxioms along an injection.

                                            Equations
                                            Instances For
                                              @[reducible, inline]
                                              abbrev Function.Injective.coframeMinimalAxioms {α : Type u} {β : Type v} [Sup α] [Inf α] [SupSet α] [InfSet α] [Top α] [Bot α] (minAx : Order.Coframe.MinimalAxioms β) (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_sSup : ∀ (s : Set α), f (sSup s) = as, f a) (map_sInf : ∀ (s : Set α), f (sInf s) = as, f a) (map_top : f = ) (map_bot : f = ) :

                                              Pullback an Order.Coframe.MinimalAxioms along an injection.

                                              Equations
                                              Instances For
                                                @[reducible, inline]
                                                abbrev Function.Injective.frame {α : Type u} {β : Type v} [Sup α] [Inf α] [SupSet α] [InfSet α] [Top α] [Bot α] [HasCompl α] [HImp α] [Order.Frame β] (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_sSup : ∀ (s : Set α), f (sSup s) = as, f a) (map_sInf : ∀ (s : Set α), f (sInf s) = as, f a) (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 an Order.Frame along an injection.

                                                Equations
                                                Instances For
                                                  @[reducible, inline]
                                                  abbrev Function.Injective.coframe {α : Type u} {β : Type v} [Sup α] [Inf α] [SupSet α] [InfSet α] [Top α] [Bot α] [HNot α] [SDiff α] [Order.Coframe β] (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_sSup : ∀ (s : Set α), f (sSup s) = as, f a) (map_sInf : ∀ (s : Set α), f (sInf s) = as, f a) (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 an Order.Coframe along an injection.

                                                  Equations
                                                  Instances For
                                                    @[reducible, inline]
                                                    abbrev Function.Injective.completeDistribLatticeMinimalAxioms {α : Type u} {β : Type v} [Sup α] [Inf α] [SupSet α] [InfSet α] [Top α] [Bot α] (minAx : CompleteDistribLattice.MinimalAxioms β) (f : αβ) (hf : Function.Injective f) (map_sup : let x := minAx.toCompleteLattice; ∀ (a b : α), f (a b) = f a f b) (map_inf : let x := minAx.toCompleteLattice; ∀ (a b : α), f (a b) = f a f b) (map_sSup : let x := minAx.toCompleteLattice; ∀ (s : Set α), f (sSup s) = as, f a) (map_sInf : let x := minAx.toCompleteLattice; ∀ (s : Set α), f (sInf s) = as, f a) (map_top : let x := minAx.toCompleteLattice; f = ) (map_bot : let x := minAx.toCompleteLattice; f = ) :

                                                    Pullback a CompleteDistribLattice.MinimalAxioms along an injection.

                                                    Equations
                                                    • One or more equations did not get rendered due to their size.
                                                    Instances For
                                                      @[reducible, inline]
                                                      abbrev Function.Injective.completeDistribLattice {α : Type u} {β : Type v} [Sup α] [Inf α] [SupSet α] [InfSet α] [Top α] [Bot α] [HasCompl α] [HImp α] [HNot α] [SDiff α] [CompleteDistribLattice β] (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_sSup : ∀ (s : Set α), f (sSup s) = as, f a) (map_sInf : ∀ (s : Set α), f (sInf s) = as, f a) (map_top : f = ) (map_bot : f = ) (map_compl : ∀ (a : α), f a = (f a)) (map_himp : ∀ (a b : α), f (a b) = f a f b) (map_hnot : ∀ (a : α), f (a) = f a) (map_sdiff : ∀ (a b : α), f (a \ b) = f a \ f b) :

                                                      Pullback a CompleteDistribLattice along an injection.

                                                      Equations
                                                      Instances For
                                                        @[reducible, inline]
                                                        abbrev Function.Injective.completelyDistribLatticeMinimalAxioms {α : Type u} {β : Type v} [Sup α] [Inf α] [SupSet α] [InfSet α] [Top α] [Bot α] (minAx : CompletelyDistribLattice.MinimalAxioms β) (f : αβ) (hf : Function.Injective f) (map_sup : let x := minAx.toCompleteLattice; ∀ (a b : α), f (a b) = f a f b) (map_inf : let x := minAx.toCompleteLattice; ∀ (a b : α), f (a b) = f a f b) (map_sSup : let x := minAx.toCompleteLattice; ∀ (s : Set α), f (sSup s) = as, f a) (map_sInf : let x := minAx.toCompleteLattice; ∀ (s : Set α), f (sInf s) = as, f a) (map_top : let x := minAx.toCompleteLattice; f = ) (map_bot : let x := minAx.toCompleteLattice; f = ) :

                                                        Pullback a CompletelyDistribLattice.MinimalAxioms along an injection.

                                                        Equations
                                                        • One or more equations did not get rendered due to their size.
                                                        Instances For
                                                          @[reducible, inline]
                                                          abbrev Function.Injective.completelyDistribLattice {α : Type u} {β : Type v} [Sup α] [Inf α] [SupSet α] [InfSet α] [Top α] [Bot α] [HasCompl α] [HImp α] [HNot α] [SDiff α] [CompletelyDistribLattice β] (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_sSup : ∀ (s : Set α), f (sSup s) = as, f a) (map_sInf : ∀ (s : Set α), f (sInf s) = as, f a) (map_top : f = ) (map_bot : f = ) (map_compl : ∀ (a : α), f a = (f a)) (map_himp : ∀ (a b : α), f (a b) = f a f b) (map_hnot : ∀ (a : α), f (a) = f a) (map_sdiff : ∀ (a b : α), f (a \ b) = f a \ f b) :

                                                          Pullback a CompletelyDistribLattice along an injection.

                                                          Equations
                                                          Instances For
                                                            @[reducible, inline]
                                                            abbrev Function.Injective.completeBooleanAlgebra {α : Type u} {β : Type v} [Sup α] [Inf α] [SupSet α] [InfSet α] [Top α] [Bot α] [HasCompl α] [HImp α] [SDiff α] [CompleteBooleanAlgebra β] (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_sSup : ∀ (s : Set α), f (sSup s) = as, f a) (map_sInf : ∀ (s : Set α), f (sInf s) = as, f a) (map_top : f = ) (map_bot : f = ) (map_compl : ∀ (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 CompleteBooleanAlgebra along an injection.

                                                            Equations
                                                            Instances For
                                                              @[reducible, inline]
                                                              abbrev Function.Injective.completeAtomicBooleanAlgebra {α : Type u} {β : Type v} [Sup α] [Inf α] [SupSet α] [InfSet α] [Top α] [Bot α] [HasCompl α] [HImp α] [HNot α] [SDiff α] [CompleteAtomicBooleanAlgebra β] (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_sSup : ∀ (s : Set α), f (sSup s) = as, f a) (map_sInf : ∀ (s : Set α), f (sInf s) = as, f a) (map_top : f = ) (map_bot : f = ) (map_compl : ∀ (a : α), f a = (f a)) (map_himp : ∀ (a b : α), f (a b) = f a f b) (map_hnot : ∀ (a : α), f (a) = f a) (map_sdiff : ∀ (a b : α), f (a \ b) = f a \ f b) :

                                                              Pullback a CompleteAtomicBooleanAlgebra along an injection.

                                                              Equations
                                                              Instances For