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.

    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.

        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

          A frame, aka complete Heyting algebra, is a complete lattice whose 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 .

              A coframe, aka complete Brouwer algebra or complete co-Heyting algebra, is a complete lattice whose 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.

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

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

                        In a complete distributive lattice, 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.

                          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.

                            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
                              @[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
                              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
                              @[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

                              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 := }
                              @[reducible, inline]

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

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

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

                              Equations
                              @[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
                              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 := }

                              The CompletelyDistribLattice.MinimalAxioms element corresponding to a frame.

                              Equations
                              • CompletelyDistribLattice.MinimalAxioms.of = { toCompleteLattice := CompletelyDistribLattice.toCompleteLattice, iInf_iSup_eq := }
                              @[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
                              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

                              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.

                                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.

                                    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
                                      @[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
                                      @[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
                                      @[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
                                      @[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.
                                      @[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
                                      @[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.
                                      @[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
                                      @[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
                                      @[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