Documentation

Mathlib.Order.CompleteBooleanAlgebra

Frames, completely distributive lattices and Boolean algebras #

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

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.

TODO #

Add instances for Prod

References #

class Order.Frame (α : Type u_1) extends CompleteLattice :
Type u_1
  • In a frame, ⊓⊓ distributes over ⨆⨆.

    inf_supₛ_le_supᵢ_inf : ∀ (a : α) (s : Set α), a supₛ s b, h, a b

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
    • In a coframe, ⊔⊔ distributes over ⨅⨅.

      infᵢ_sup_le_sup_infₛ : ∀ (a : α) (s : Set α), (b, h, a b) a infₛ s

    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
      • In a completely distributive lattice, ⊔⊔ distributes over ⨅⨅.

        infᵢ_sup_le_sup_infₛ : ∀ (a : α) (s : Set α), (b, h, a b) a infₛ s

      A completely distributive lattice is a complete lattice whose ⊔⊔ and ⊓⊓ respectively distribute over ⨅⨅ and ⨆⨆.

      Instances
        Equations
        instance OrderDual.coframe {α : Type u} [inst : Order.Frame α] :
        Equations
        theorem inf_supₛ_eq {α : Type u} [inst : Order.Frame α] {s : Set α} {a : α} :
        a supₛ s = b, h, a b
        theorem supₛ_inf_eq {α : Type u} [inst : Order.Frame α] {s : Set α} {b : α} :
        supₛ s b = a, h, a b
        theorem supᵢ_inf_eq {α : Type u} {ι : Sort w} [inst : Order.Frame α] (f : ια) (a : α) :
        (i, f i) a = i, f i a
        theorem inf_supᵢ_eq {α : Type u} {ι : Sort w} [inst : Order.Frame α] (a : α) (f : ια) :
        (a i, f i) = i, a f i
        theorem supᵢ₂_inf_eq {α : Type u} {ι : Sort w} {κ : ιSort u_1} [inst : Order.Frame α] {f : (i : ι) → κ iα} (a : α) :
        (i, j, f i j) a = i, j, f i j a
        theorem inf_supᵢ₂_eq {α : Type u} {ι : Sort w} {κ : ιSort u_1} [inst : Order.Frame α] {f : (i : ι) → κ iα} (a : α) :
        (a i, j, f i j) = i, j, a f i j
        theorem supᵢ_inf_supᵢ {α : Type u} [inst : Order.Frame α] {ι : Type u_1} {ι' : Type u_2} {f : ια} {g : ι'α} :
        ((i, f i) j, g j) = i, f i.fst g i.snd
        theorem bsupᵢ_inf_bsupᵢ {α : Type u} [inst : Order.Frame α] {ι : Type u_1} {ι' : Type u_2} {f : ια} {g : ι'α} {s : Set ι} {t : Set ι'} :
        ((i, h, f i) j, h, g j) = p, h, f p.fst g p.snd
        theorem supₛ_inf_supₛ {α : Type u} [inst : Order.Frame α] {s : Set α} {t : Set α} :
        supₛ s supₛ t = p, h, p.fst p.snd
        theorem supᵢ_disjoint_iff {α : Type u} {ι : Sort w} [inst : Order.Frame α] {a : α} {f : ια} :
        Disjoint (i, f i) a ∀ (i : ι), Disjoint (f i) a
        theorem disjoint_supᵢ_iff {α : Type u} {ι : Sort w} [inst : Order.Frame α] {a : α} {f : ια} :
        Disjoint a (i, f i) ∀ (i : ι), Disjoint a (f i)
        theorem supᵢ₂_disjoint_iff {α : Type u} {ι : Sort w} {κ : ιSort u_1} [inst : Order.Frame α] {a : α} {f : (i : ι) → κ iα} :
        Disjoint (i, j, f i j) a ∀ (i : ι) (j : κ i), Disjoint (f i j) a
        theorem disjoint_supᵢ₂_iff {α : Type u} {ι : Sort w} {κ : ιSort u_1} [inst : Order.Frame α] {a : α} {f : (i : ι) → κ iα} :
        Disjoint a (i, j, f i j) ∀ (i : ι) (j : κ i), Disjoint a (f i j)
        theorem supₛ_disjoint_iff {α : Type u} [inst : Order.Frame α] {a : α} {s : Set α} :
        Disjoint (supₛ s) a ∀ (b : α), b sDisjoint b a
        theorem disjoint_supₛ_iff {α : Type u} [inst : Order.Frame α] {a : α} {s : Set α} :
        Disjoint a (supₛ s) ∀ (b : α), b sDisjoint a b
        theorem supᵢ_inf_of_monotone {α : Type u} [inst : Order.Frame α] {ι : Type u_1} [inst : Preorder ι] [inst : 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 supᵢ_inf_of_antitone {α : Type u} [inst : Order.Frame α] {ι : Type u_1} [inst : Preorder ι] [inst : 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} [inst : (i : ι) → Order.Frame (π i)] :
        Order.Frame ((i : ι) → π i)
        Equations
        • One or more equations did not get rendered due to their size.
        instance Frame.toDistribLattice {α : Type u} [inst : Order.Frame α] :
        Equations
        instance OrderDual.frame {α : Type u} [inst : Order.Coframe α] :
        Equations
        theorem sup_infₛ_eq {α : Type u} [inst : Order.Coframe α] {s : Set α} {a : α} :
        a infₛ s = b, h, a b
        theorem infₛ_sup_eq {α : Type u} [inst : Order.Coframe α] {s : Set α} {b : α} :
        infₛ s b = a, h, a b
        theorem infᵢ_sup_eq {α : Type u} {ι : Sort w} [inst : Order.Coframe α] (f : ια) (a : α) :
        (i, f i) a = i, f i a
        theorem sup_infᵢ_eq {α : Type u} {ι : Sort w} [inst : Order.Coframe α] (a : α) (f : ια) :
        (a i, f i) = i, a f i
        theorem infᵢ₂_sup_eq {α : Type u} {ι : Sort w} {κ : ιSort u_1} [inst : Order.Coframe α] {f : (i : ι) → κ iα} (a : α) :
        (i, j, f i j) a = i, j, f i j a
        theorem sup_infᵢ₂_eq {α : Type u} {ι : Sort w} {κ : ιSort u_1} [inst : Order.Coframe α] {f : (i : ι) → κ iα} (a : α) :
        (a i, j, f i j) = i, j, a f i j
        theorem infᵢ_sup_infᵢ {α : Type u} [inst : Order.Coframe α] {ι : Type u_1} {ι' : Type u_2} {f : ια} {g : ι'α} :
        ((i, f i) i, g i) = i, f i.fst g i.snd
        theorem binfᵢ_sup_binfᵢ {α : Type u} [inst : Order.Coframe α] {ι : Type u_1} {ι' : Type u_2} {f : ια} {g : ι'α} {s : Set ι} {t : Set ι'} :
        ((i, h, f i) j, h, g j) = p, h, f p.fst g p.snd
        theorem infₛ_sup_infₛ {α : Type u} [inst : Order.Coframe α] {s : Set α} {t : Set α} :
        infₛ s infₛ t = p, h, p.fst p.snd
        theorem infᵢ_sup_of_monotone {α : Type u} [inst : Order.Coframe α] {ι : Type u_1} [inst : Preorder ι] [inst : 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 infᵢ_sup_of_antitone {α : Type u} [inst : Order.Coframe α] {ι : Type u_1} [inst : Preorder ι] [inst : 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} [inst : (i : ι) → Order.Coframe (π i)] :
        Order.Coframe ((i : ι) → π i)
        Equations
        • One or more equations did not get rendered due to their size.
        instance Coframe.toDistribLattice {α : Type u} [inst : Order.Coframe α] :
        Equations
        Equations
        instance Pi.completeDistribLattice {ι : Type u_1} {π : ιType u_2} [inst : (i : ι) → CompleteDistribLattice (π i)] :
        CompleteDistribLattice ((i : ι) → π i)
        Equations
        class CompleteBooleanAlgebra (α : Type u_1) extends BooleanAlgebra , SupSet , InfSet :
        Type u_1
        • Any upper bound is more than the set supremum.

          supₛ_le : ∀ (s : Set α) (a : α), (∀ (b : α), b sb a) → supₛ s a
        • toInfSet : InfSet α
        • Any element of a set is more than the set infimum.

          infₛ_le : ∀ (s : Set α) (a : α), a sinfₛ s a
        • Any lower bound is less than the set infimum.

          le_infₛ : ∀ (s : Set α) (a : α), (∀ (b : α), b sa b) → a infₛ s
        • In a frame, ⊓⊓ distributes over ⨆⨆.

          inf_supₛ_le_supᵢ_inf : ∀ (a : α) (s : Set α), a supₛ s b, h, a b
        • In a completely distributive lattice, ⊔⊔ distributes over ⨅⨅.

          infᵢ_sup_le_sup_infₛ : ∀ (a : α) (s : Set α), (b, h, a b) a infₛ s

        A complete Boolean algebra is a completely distributive Boolean algebra.

        Instances
          instance Pi.completeBooleanAlgebra {ι : Type u_1} {π : ιType u_2} [inst : (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_infᵢ {α : Type u} {ι : Sort w} [inst : CompleteBooleanAlgebra α] {f : ια} :
          infᵢ f = i, f i
          theorem compl_supᵢ {α : Type u} {ι : Sort w} [inst : CompleteBooleanAlgebra α] {f : ια} :
          supᵢ f = i, f i
          theorem compl_infₛ {α : Type u} [inst : CompleteBooleanAlgebra α] {s : Set α} :
          infₛ s = i, h, i
          theorem compl_supₛ {α : Type u} [inst : CompleteBooleanAlgebra α] {s : Set α} :
          supₛ s = i, h, i
          theorem compl_infₛ' {α : Type u} [inst : CompleteBooleanAlgebra α] {s : Set α} :
          infₛ s = supₛ (compl '' s)
          theorem compl_supₛ' {α : Type u} [inst : CompleteBooleanAlgebra α] {s : Set α} :
          supₛ s = infₛ (compl '' s)
          def Function.Injective.frame {α : Type u} {β : Type v} [inst : Sup α] [inst : Inf α] [inst : SupSet α] [inst : InfSet α] [inst : Top α] [inst : Bot α] [inst : 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_supₛ : ∀ (s : Set α), f (supₛ s) = a, h, f a) (map_infₛ : ∀ (s : Set α), f (infₛ s) = a, h, 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.
          def Function.Injective.coframe {α : Type u} {β : Type v} [inst : Sup α] [inst : Inf α] [inst : SupSet α] [inst : InfSet α] [inst : Top α] [inst : Bot α] [inst : 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_supₛ : ∀ (s : Set α), f (supₛ s) = a, h, f a) (map_infₛ : ∀ (s : Set α), f (infₛ s) = a, h, 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.
          def Function.Injective.completeDistribLattice {α : Type u} {β : Type v} [inst : Sup α] [inst : Inf α] [inst : SupSet α] [inst : InfSet α] [inst : Top α] [inst : Bot α] [inst : 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_supₛ : ∀ (s : Set α), f (supₛ s) = a, h, f a) (map_infₛ : ∀ (s : Set α), f (infₛ s) = a, h, 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.
          def Function.Injective.completeBooleanAlgebra {α : Type u} {β : Type v} [inst : Sup α] [inst : Inf α] [inst : SupSet α] [inst : InfSet α] [inst : Top α] [inst : Bot α] [inst : HasCompl α] [inst : SDiff α] [inst : 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_supₛ : ∀ (s : Set α), f (supₛ s) = a, h, f a) (map_infₛ : ∀ (s : Set α), f (infₛ s) = a, h, 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.
          Equations
          • One or more equations did not get rendered due to their size.