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 #

class Order.Frame (α : Type u_1) extends CompleteLattice :
Type u_1
  • 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_1 : Set α) (a : α), a s_1a sSup s_1
  • sSup_le : ∀ (s_1 : Set α) (a : α), (∀ (b : α), b s_1b a) → sSup s_1 a
  • sInf : Set αα
  • sInf_le : ∀ (s_1 : Set α) (a : α), a s_1sInf s_1 a
  • le_sInf : ∀ (s_1 : Set α) (a : α), (∀ (b : α), b s_1a b) → a sInf s_1
  • top : α
  • bot : α
  • le_top : ∀ (x : α), x
  • bot_le : ∀ (x : α), x
  • inf_sSup_le_iSup_inf : ∀ (a : α) (s_1 : Set α), a sSup s_1 ⨆ (b : α) (_ : b s_1), a b

    In a frame, distributes over .

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

Instances
    class Order.Coframe (α : Type u_1) extends CompleteLattice :
    Type u_1
    • 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_1 : Set α) (a : α), a s_1a sSup s_1
    • sSup_le : ∀ (s_1 : Set α) (a : α), (∀ (b : α), b s_1b a) → sSup s_1 a
    • sInf : Set αα
    • sInf_le : ∀ (s_1 : Set α) (a : α), a s_1sInf s_1 a
    • le_sInf : ∀ (s_1 : Set α) (a : α), (∀ (b : α), b s_1a b) → a sInf s_1
    • top : α
    • bot : α
    • le_top : ∀ (x : α), x
    • bot_le : ∀ (x : α), x
    • iInf_sup_le_sup_sInf : ∀ (a : α) (s_1 : Set α), ⨅ (b : α) (_ : b s_1), a b a sInf s_1

      In a coframe, distributes over .

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

    Instances
      class CompleteDistribLattice (α : Type u_1) extends Order.Frame :
      Type u_1
      • 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_1 : Set α) (a : α), a s_1a sSup s_1
      • sSup_le : ∀ (s_1 : Set α) (a : α), (∀ (b : α), b s_1b a) → sSup s_1 a
      • sInf : Set αα
      • sInf_le : ∀ (s_1 : Set α) (a : α), a s_1sInf s_1 a
      • le_sInf : ∀ (s_1 : Set α) (a : α), (∀ (b : α), b s_1a b) → a sInf s_1
      • top : α
      • bot : α
      • le_top : ∀ (x : α), x
      • bot_le : ∀ (x : α), x
      • inf_sSup_le_iSup_inf : ∀ (a : α) (s_1 : Set α), a sSup s_1 ⨆ (b : α) (_ : b s_1), a b
      • iInf_sup_le_sup_sInf : ∀ (a : α) (s_1 : Set α), ⨅ (b : α) (_ : b s_1), a b a sInf s_1

        In a complete distributive lattice, distributes over .

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

      Instances
        Equations
        • 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_1 : Set α) (a : α), a s_1a sSup s_1
        • sSup_le : ∀ (s_1 : Set α) (a : α), (∀ (b : α), b s_1b a) → sSup s_1 a
        • sInf : Set αα
        • sInf_le : ∀ (s_1 : Set α) (a : α), a s_1sInf s_1 a
        • le_sInf : ∀ (s_1 : Set α) (a : α), (∀ (b : α), b s_1a b) → a sInf s_1
        • 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)

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

        Instances
          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 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_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 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)
          Equations
          Equations
          • One or more equations did not get rendered due to their size.
          Equations
          theorem inf_sSup_eq {α : Type u} [Order.Frame α] {s : Set α} {a : α} :
          a sSup s = ⨆ (b : α) (_ : b s), a b
          theorem sSup_inf_eq {α : Type u} [Order.Frame α] {s : Set α} {b : α} :
          sSup s b = ⨆ (a : α) (_ : a s), 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
          instance Prod.frame (α : Type u_1) (β : Type u_2) [Order.Frame α] [Order.Frame β] :
          Order.Frame (α × β)
          Equations
          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.fst g i.snd
          theorem biSup_inf_biSup {α : Type u} [Order.Frame α] {ι : Type u_1} {ι' : Type u_2} {f : ια} {g : ι'α} {s : Set ι} {t : Set ι'} :
          (⨆ (i : ι) (_ : i s), f i) ⨆ (j : ι') (_ : j t), g j = ⨆ (p : ι × ι') (_ : p s ×ˢ t), f p.fst g p.snd
          theorem sSup_inf_sSup {α : Type u} [Order.Frame α] {s : Set α} {t : Set α} :
          sSup s sSup t = ⨆ (p : α × α) (_ : p s ×ˢ t), p.fst p.snd
          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 ∀ (b : α), b sDisjoint b a
          theorem disjoint_sSup_iff {α : Type u} [Order.Frame α] {a : α} {s : Set α} :
          Disjoint a (sSup s) ∀ (b : α), b sDisjoint a b
          theorem iSup_inf_of_monotone {α : Type u} [Order.Frame α] {ι : Type u_1} [Preorder ι] [IsDirected ι fun x x_1 => x x_1] {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 x x_1 => x x_1)] {f : ια} {g : ια} (hf : Antitone f) (hg : Antitone g) :
          ⨆ (i : ι), f i g i = (⨆ (i : ι), f i) ⨆ (i : ι), g i
          instance Pi.frame {ι : Type u_1} {π : ιType u_2} [(i : ι) → Order.Frame (π i)] :
          Order.Frame ((i : ι) → π i)
          Equations
          • One or more equations did not get rendered due to their size.
          Equations
          Equations
          theorem sup_sInf_eq {α : Type u} [Order.Coframe α] {s : Set α} {a : α} :
          a sInf s = ⨅ (b : α) (_ : b s), a b
          theorem sInf_sup_eq {α : Type u} [Order.Coframe α] {s : Set α} {b : α} :
          sInf s b = ⨅ (a : α) (_ : a s), 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
          instance Prod.coframe (α : Type u_1) (β : Type u_2) [Order.Coframe α] [Order.Coframe β] :
          Equations
          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.fst g i.snd
          theorem biInf_sup_biInf {α : Type u} [Order.Coframe α] {ι : Type u_1} {ι' : Type u_2} {f : ια} {g : ι'α} {s : Set ι} {t : Set ι'} :
          (⨅ (i : ι) (_ : i s), f i) ⨅ (j : ι') (_ : j t), g j = ⨅ (p : ι × ι') (_ : p s ×ˢ t), f p.fst g p.snd
          theorem sInf_sup_sInf {α : Type u} [Order.Coframe α] {s : Set α} {t : Set α} :
          sInf s sInf t = ⨅ (p : α × α) (_ : p s ×ˢ t), p.fst p.snd
          theorem iInf_sup_of_monotone {α : Type u} [Order.Coframe α] {ι : Type u_1} [Preorder ι] [IsDirected ι (Function.swap fun x x_1 => x x_1)] {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 x x_1 => x x_1] {f : ια} {g : ια} (hf : Antitone f) (hg : Antitone g) :
          ⨅ (i : ι), f i g i = (⨅ (i : ι), f i) ⨅ (i : ι), g i
          instance Pi.coframe {ι : Type u_1} {π : ιType u_2} [(i : ι) → Order.Coframe (π i)] :
          Order.Coframe ((i : ι) → π i)
          Equations
          • One or more equations did not get rendered due to their size.
          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.completeDistribLattice {ι : Type u_1} {π : ιType u_2} [(i : ι) → CompleteDistribLattice (π i)] :
          CompleteDistribLattice ((i : ι) → π i)
          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.
          Equations
          • One or more equations did not get rendered due to their size.
          instance Pi.completelyDistribLattice {ι : Type u_1} {π : ιType u_2} [(i : ι) → CompletelyDistribLattice (π i)] :
          CompletelyDistribLattice ((i : ι) → π i)
          Equations
          • One or more equations did not get rendered due to their size.
          class CompleteBooleanAlgebra (α : Type u_1) extends BooleanAlgebra , SupSet , InfSet :
          Type u_1
          • 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
          • le_sup_inf : ∀ (x y z : α), (x y) (x z) x y z
          • compl : αα
          • sdiff : ααα
          • himp : ααα
          • top : α
          • bot : α
          • inf_compl_le_bot : ∀ (x : α), x x
          • top_le_sup_compl : ∀ (x : α), x x
          • le_top : ∀ (a : α), a
          • bot_le : ∀ (a : α), a
          • sdiff_eq : ∀ (x y : α), x \ y = x y
          • himp_eq : ∀ (x y : α), x y = y x
          • sSup : Set αα
          • le_sSup : ∀ (s_1 : Set α) (a : α), a s_1a sSup s_1

            Any element of a set is less than the set supremum.

          • sSup_le : ∀ (s_1 : Set α) (a : α), (∀ (b : α), b s_1b a) → sSup s_1 a

            Any upper bound is more than the set supremum.

          • sInf : Set αα
          • sInf_le : ∀ (s_1 : Set α) (a : α), a s_1sInf s_1 a

            Any element of a set is more than the set infimum.

          • le_sInf : ∀ (s_1 : Set α) (a : α), (∀ (b : α), b s_1a b) → a sInf s_1

            Any lower bound is less than the set infimum.

          • inf_sSup_le_iSup_inf : ∀ (a : α) (s_1 : Set α), a sSup s_1 ⨆ (b : α) (_ : b s_1), a b

            In a frame, distributes over .

          • iInf_sup_le_sup_sInf : ∀ (a : α) (s_1 : Set α), ⨅ (b : α) (_ : b s_1), a b a sInf s_1

            In a complete distributive lattice, distributes over .

          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
            Equations
            • One or more equations did not get rendered due to their size.
            instance Pi.completeBooleanAlgebra {ι : Type u_1} {π : ιType u_2} [(i : ι) → CompleteBooleanAlgebra (π i)] :
            CompleteBooleanAlgebra ((i : ι) → π i)
            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.
            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) = ⨆ (i : α) (_ : i s), i
            theorem compl_sSup {α : Type u} [CompleteBooleanAlgebra α] {s : Set α} :
            (sSup s) = ⨅ (i : α) (_ : i s), 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)
            • 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_1 : Set α) (a : α), a s_1a sSup s_1
            • sSup_le : ∀ (s_1 : Set α) (a : α), (∀ (b : α), b s_1b a) → sSup s_1 a
            • sInf : Set αα
            • sInf_le : ∀ (s_1 : Set α) (a : α), a s_1sInf s_1 a
            • le_sInf : ∀ (s_1 : Set α) (a : α), (∀ (b : α), b s_1a b) → a sInf s_1
            • 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)
            • 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_1 : Set α), a sSup s_1 ⨆ (b : α) (_ : b s_1), a b

              In a frame, distributes over .

            • iInf_sup_le_sup_sInf : ∀ (a : α) (s_1 : Set α), ⨅ (b : α) (_ : b s_1), a b a sInf s_1

              In a complete distributive lattice, distributes over .

            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
              Equations
              • One or more equations did not get rendered due to their size.
              instance Pi.completeAtomicBooleanAlgebra {ι : Type u_1} {π : ιType u_2} [(i : ι) → CompleteAtomicBooleanAlgebra (π i)] :
              CompleteAtomicBooleanAlgebra ((i : ι) → π i)
              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.
              Equations
              • One or more equations did not get rendered due to their size.
              @[reducible]
              def Function.Injective.frame {α : Type u} {β : Type v} [Sup α] [Inf α] [SupSet α] [InfSet α] [Top α] [Bot α] [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) = ⨆ (a : α) (_ : a s), f a) (map_sInf : ∀ (s : Set α), f (sInf s) = ⨅ (a : α) (_ : a s), f a) (map_top : f = ) (map_bot : f = ) :

              Pullback an Order.Frame along an injection.

              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                @[reducible]
                def Function.Injective.coframe {α : Type u} {β : Type v} [Sup α] [Inf α] [SupSet α] [InfSet α] [Top α] [Bot α] [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) = ⨆ (a : α) (_ : a s), f a) (map_sInf : ∀ (s : Set α), f (sInf s) = ⨅ (a : α) (_ : a s), f a) (map_top : f = ) (map_bot : f = ) :

                Pullback an Order.Coframe along an injection.

                Equations
                • One or more equations did not get rendered due to their size.
                Instances For
                  @[reducible]
                  def Function.Injective.completeDistribLattice {α : Type u} {β : Type v} [Sup α] [Inf α] [SupSet α] [InfSet α] [Top α] [Bot α] [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) = ⨆ (a : α) (_ : a s), f a) (map_sInf : ∀ (s : Set α), f (sInf s) = ⨅ (a : α) (_ : a s), f a) (map_top : f = ) (map_bot : f = ) :

                  Pullback a CompleteDistribLattice along an injection.

                  Equations
                  • One or more equations did not get rendered due to their size.
                  Instances For
                    @[reducible]
                    def Function.Injective.completelyDistribLattice {α : Type u} {β : Type v} [Sup α] [Inf α] [SupSet α] [InfSet α] [Top α] [Bot α] [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) = ⨆ (a : α) (_ : a s), f a) (map_sInf : ∀ (s : Set α), f (sInf s) = ⨅ (a : α) (_ : a s), f a) (map_top : f = ) (map_bot : f = ) :

                    Pullback a CompletelyDistribLattice along an injection.

                    Equations
                    • One or more equations did not get rendered due to their size.
                    Instances For
                      @[reducible]
                      def Function.Injective.completeBooleanAlgebra {α : Type u} {β : Type v} [Sup α] [Inf α] [SupSet α] [InfSet α] [Top α] [Bot α] [HasCompl α] [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) = ⨆ (a : α) (_ : a s), f a) (map_sInf : ∀ (s : Set α), f (sInf s) = ⨅ (a : α) (_ : a s), f a) (map_top : f = ) (map_bot : f = ) (map_compl : ∀ (a : α), f a = (f a)) (map_sdiff : ∀ (a b : α), f (a \ b) = f a \ f b) :

                      Pullback a CompleteBooleanAlgebra along an injection.

                      Equations
                      • One or more equations did not get rendered due to their size.
                      Instances For
                        @[reducible]
                        def Function.Injective.completeAtomicBooleanAlgebra {α : Type u} {β : Type v} [Sup α] [Inf α] [SupSet α] [InfSet α] [Top α] [Bot α] [HasCompl α] [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) = ⨆ (a : α) (_ : a s), f a) (map_sInf : ∀ (s : Set α), f (sInf s) = ⨅ (a : α) (_ : a s), f a) (map_top : f = ) (map_bot : f = ) (map_compl : ∀ (a : α), f a = (f a)) (map_sdiff : ∀ (a b : α), f (a \ b) = f a \ f b) :

                        Pullback a CompleteAtomicBooleanAlgebra along an injection.

                        Equations
                        • One or more equations did not get rendered due to their size.
                        Instances For
                          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.