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

• Order.Frame: Frame: A complete lattice whose ⊓ distributes over ⨆.
• Order.Coframe: Coframe: A complete lattice whose ⊔ distributes over ⨅.
• CompleteDistribLattice: Complete distributive lattices: A complete lattice whose ⊓ and ⊔ distribute over ⨆ and ⨅ respectively.
• CompleteBooleanAlgebra: Complete Boolean algebra: A Boolean algebra whose ⊓ and ⊔ distribute over ⨆ and ⨅ respectively.
• CompletelyDistribLattice: Completely distributive lattices: A complete lattice whose ⨅ and ⨆ satisfy iInf_iSup_eq.
• CompleteBooleanAlgebra: Complete Boolean algebra: A Boolean algebra whose ⊓ and ⊔ distribute over ⨆ and ⨅ respectively.
• CompleteAtomicBooleanAlgebra: Complete atomic Boolean algebra: A complete Boolean algebra which is additionally completely distributive. (This implies that it's (co)atom(ist)ic.)

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

• Wikipedia, Complete Heyting algebra
• [Francis Borceux, Handbook of Categorical Algebra III][borceux-vol3]

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 ≤ b → b ≤ c → a ≤ c
• lt_iff_le_not_le : ∀ (a b : α), a < b ↔ a ≤ b ∧ ¬b ≤ a
• le_antisymm : ∀ (a b : α), a ≤ b → b ≤ a → a = b
• le_sup_left : ∀ (a b : α), a ≤ a ⊔ b
• le_sup_right : ∀ (a b : α), b ≤ a ⊔ b
• sup_le : ∀ (a b c : α), a ≤ c → b ≤ c → a ⊔ 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 ≤ b → a ≤ c → a ≤ b ⊓ c
• sSup : Set α → α
• le_sSup : ∀ (s_1 : Set α) (a : α), a ∈ s_1 → a ≤ sSup s_1
• sSup_le : ∀ (s_1 : Set α) (a : α), (∀ (b : α), b ∈ s_1 → b ≤ a) → sSup s_1 ≤ a
• sInf : Set α → α
• sInf_le : ∀ (s_1 : Set α) (a : α), a ∈ s_1 → sInf s_1 ≤ a
• le_sInf : ∀ (s_1 : Set α) (a : α), (∀ (b : α), b ∈ s_1 → a ≤ 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 ⨆.

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 ≤ b → b ≤ c → a ≤ c
• lt_iff_le_not_le : ∀ (a b : α), a < b ↔ a ≤ b ∧ ¬b ≤ a
• le_antisymm : ∀ (a b : α), a ≤ b → b ≤ a → a = b
• le_sup_left : ∀ (a b : α), a ≤ a ⊔ b
• le_sup_right : ∀ (a b : α), b ≤ a ⊔ b
• sup_le : ∀ (a b c : α), a ≤ c → b ≤ c → a ⊔ 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 ≤ b → a ≤ c → a ≤ b ⊓ c
• sSup : Set α → α
• le_sSup : ∀ (s_1 : Set α) (a : α), a ∈ s_1 → a ≤ sSup s_1
• sSup_le : ∀ (s_1 : Set α) (a : α), (∀ (b : α), b ∈ s_1 → b ≤ a) → sSup s_1 ≤ a
• sInf : Set α → α
• sInf_le : ∀ (s_1 : Set α) (a : α), a ∈ s_1 → sInf s_1 ≤ a
• le_sInf : ∀ (s_1 : Set α) (a : α), (∀ (b : α), b ∈ s_1 → a ≤ 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 ⨅.

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 ≤ b → b ≤ c → a ≤ c
• lt_iff_le_not_le : ∀ (a b : α), a < b ↔ a ≤ b ∧ ¬b ≤ a
• le_antisymm : ∀ (a b : α), a ≤ b → b ≤ a → a = b
• le_sup_left : ∀ (a b : α), a ≤ a ⊔ b
• le_sup_right : ∀ (a b : α), b ≤ a ⊔ b
• sup_le : ∀ (a b c : α), a ≤ c → b ≤ c → a ⊔ 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 ≤ b → a ≤ c → a ≤ b ⊓ c
• sSup : Set α → α
• le_sSup : ∀ (s_1 : Set α) (a : α), a ∈ s_1 → a ≤ sSup s_1
• sSup_le : ∀ (s_1 : Set α) (a : α), (∀ (b : α), b ∈ s_1 → b ≤ a) → sSup s_1 ≤ a
• sInf : Set α → α
• sInf_le : ∀ (s_1 : Set α) (a : α), a ∈ s_1 → sInf s_1 ≤ a
• le_sInf : ∀ (s_1 : Set α) (a : α), (∀ (b : α), b ∈ s_1 → a ≤ 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 ⨆.

instance CompleteDistribLattice.toCoframe {α : Type u} [CompleteDistribLattice α] : Order.Coframe α

class CompletelyDistribLattice (α : Type u) extends CompleteLattice : Type u

• sup : α → α → α
• le : α → α → Prop
• lt : α → α → Prop
• le_refl : ∀ (a : α), a ≤ a
• le_trans : ∀ (a b c : α), a ≤ b → b ≤ c → a ≤ c
• lt_iff_le_not_le : ∀ (a b : α), a < b ↔ a ≤ b ∧ ¬b ≤ a
• le_antisymm : ∀ (a b : α), a ≤ b → b ≤ a → a = b
• le_sup_left : ∀ (a b : α), a ≤ a ⊔ b
• le_sup_right : ∀ (a b : α), b ≤ a ⊔ b
• sup_le : ∀ (a b c : α), a ≤ c → b ≤ c → a ⊔ 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 ≤ b → a ≤ c → a ≤ b ⊓ c
• sSup : Set α → α
• le_sSup : ∀ (s_1 : Set α) (a : α), a ∈ s_1 → a ≤ sSup s_1
• sSup_le : ∀ (s_1 : Set α) (a : α), (∀ (b : α), b ∈ s_1 → b ≤ a) → sSup s_1 ≤ a
• sInf : Set α → α
• sInf_le : ∀ (s_1 : Set α) (a : α), a ∈ s_1 → sInf s_1 ≤ a
• le_sInf : ∀ (s_1 : Set α) (a : α), (∀ (b : α), b ∈ s_1 → a ≤ 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.

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)

instance CompletelyDistribLattice.toCompleteDistribLattice {α : Type u} [CompletelyDistribLattice α] : CompleteDistribLattice α

instance CompleteLinearOrder.toCompletelyDistribLattice {α : Type u} [CompleteLinearOrder α] : CompletelyDistribLattice α

instance OrderDual.coframe {α : Type u} [Order.Frame α] : Order.Coframe αᵒᵈ

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 (α × β)

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 ∈ s → Disjoint b a

theorem disjoint_sSup_iff {α : Type u} [Order.Frame α] {a : α} {s : Set α} : Disjoint a (sSup s) ↔ ∀ (b : α), b ∈ s → Disjoint 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)

instance Frame.toDistribLattice {α : Type u} [Order.Frame α] : DistribLattice α

instance OrderDual.frame {α : Type u} [Order.Coframe α] : Order.Frame αᵒᵈ

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 β] : Order.Coframe (α × β)

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)

instance Coframe.toDistribLattice {α : Type u} [Order.Coframe α] : DistribLattice α

instance OrderDual.completeDistribLattice (α : Type u_1) [CompleteDistribLattice α] : CompleteDistribLattice αᵒᵈ

instance Prod.completeDistribLattice (α : Type u_1) (β : Type u_2) [CompleteDistribLattice α] [CompleteDistribLattice β] : CompleteDistribLattice (α × β)

instance Pi.completeDistribLattice {ι : Type u_1} {π : ι → Type u_2} [(i : ι) → CompleteDistribLattice (π i)] : CompleteDistribLattice ((i : ι) → π i)

instance OrderDual.completelyDistribLattice (α : Type u_1) [CompletelyDistribLattice α] : CompletelyDistribLattice αᵒᵈ

instance Prod.completelyDistribLattice (α : Type u_1) (β : Type u_2) [CompletelyDistribLattice α] [CompletelyDistribLattice β] : CompletelyDistribLattice (α × β)

instance Pi.completelyDistribLattice {ι : Type u_1} {π : ι → Type u_2} [(i : ι) → CompletelyDistribLattice (π i)] : CompletelyDistribLattice ((i : ι) → π i)

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 ≤ b → b ≤ c → a ≤ c
• lt_iff_le_not_le : ∀ (a b : α), a < b ↔ a ≤ b ∧ ¬b ≤ a
• le_antisymm : ∀ (a b : α), a ≤ b → b ≤ a → a = b
• le_sup_left : ∀ (a b : α), a ≤ a ⊔ b
• le_sup_right : ∀ (a b : α), b ≤ a ⊔ b
• sup_le : ∀ (a b c : α), a ≤ c → b ≤ c → a ⊔ 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 ≤ b → a ≤ c → a ≤ 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_1 → a ≤ sSup s_1

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

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

  Any upper bound is more than the set supremum.

• sInf : Set α → α
• sInf_le : ∀ (s_1 : Set α) (a : α), a ∈ s_1 → sInf s_1 ≤ a

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

• le_sInf : ∀ (s_1 : Set α) (a : α), (∀ (b : α), b ∈ s_1 → a ≤ 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.

instance Prod.completeBooleanAlgebra (α : Type u_1) (β : Type u_2) [CompleteBooleanAlgebra α] [CompleteBooleanAlgebra β] : CompleteBooleanAlgebra (α × β)

instance Pi.completeBooleanAlgebra {ι : Type u_1} {π : ι → Type u_2} [(i : ι) → CompleteBooleanAlgebra (π i)] : CompleteBooleanAlgebra ((i : ι) → π i)

instance OrderDual.completeBooleanAlgebra (α : Type u_1) [CompleteBooleanAlgebra α] : CompleteBooleanAlgebra αᵒᵈ

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)

class CompleteAtomicBooleanAlgebra (α : Type u) extends CompletelyDistribLattice , HasCompl , SDiff , HImp : Type u

• sup : α → α → α
• le : α → α → Prop
• lt : α → α → Prop
• le_refl : ∀ (a : α), a ≤ a
• le_trans : ∀ (a b c : α), a ≤ b → b ≤ c → a ≤ c
• lt_iff_le_not_le : ∀ (a b : α), a < b ↔ a ≤ b ∧ ¬b ≤ a
• le_antisymm : ∀ (a b : α), a ≤ b → b ≤ a → a = b
• le_sup_left : ∀ (a b : α), a ≤ a ⊔ b
• le_sup_right : ∀ (a b : α), b ≤ a ⊔ b
• sup_le : ∀ (a b c : α), a ≤ c → b ≤ c → a ⊔ 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 ≤ b → a ≤ c → a ≤ b ⊓ c
• sSup : Set α → α
• le_sSup : ∀ (s_1 : Set α) (a : α), a ∈ s_1 → a ≤ sSup s_1
• sSup_le : ∀ (s_1 : Set α) (a : α), (∀ (b : α), b ∈ s_1 → b ≤ a) → sSup s_1 ≤ a
• sInf : Set α → α
• sInf_le : ∀ (s_1 : Set α) (a : α), a ∈ s_1 → sInf s_1 ≤ a
• le_sInf : ∀ (s_1 : Set α) (a : α), (∀ (b : α), b ∈ s_1 → a ≤ 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.

instance Prod.completeAtomicBooleanAlgebra (α : Type u_1) (β : Type u_2) [CompleteAtomicBooleanAlgebra α] [CompleteAtomicBooleanAlgebra β] : CompleteAtomicBooleanAlgebra (α × β)

instance Pi.completeAtomicBooleanAlgebra {ι : Type u_1} {π : ι → Type u_2} [(i : ι) → CompleteAtomicBooleanAlgebra (π i)] : CompleteAtomicBooleanAlgebra ((i : ι) → π i)

instance OrderDual.completeAtomicBooleanAlgebra (α : Type u_1) [CompleteAtomicBooleanAlgebra α] : CompleteAtomicBooleanAlgebra αᵒᵈ

instance Prop.completeAtomicBooleanAlgebra : CompleteAtomicBooleanAlgebra Prop

instance Prop.completeBooleanAlgebra : CompleteBooleanAlgebra Prop

@[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 ⊥ = ⊥) : Order.Frame α

Pullback an Order.Frame along an injection.

@[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 ⊥ = ⊥) : Order.Coframe α

Pullback an Order.Coframe along an injection.

@[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 ⊥ = ⊥) : CompleteDistribLattice α

Pullback a CompleteDistribLattice along an injection.

@[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 ⊥ = ⊥) : CompletelyDistribLattice α

Pullback a CompletelyDistribLattice along an injection.

@[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) : CompleteBooleanAlgebra α

Pullback a CompleteBooleanAlgebra along an injection.

@[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) : CompleteAtomicBooleanAlgebra α

Pullback a CompleteAtomicBooleanAlgebra along an injection.

instance PUnit.completeAtomicBooleanAlgebra : CompleteAtomicBooleanAlgebra PUnit.{u_1 + 1}

instance PUnit.completeBooleanAlgebra : CompleteBooleanAlgebra PUnit.{u_1 + 1}

instance PUnit.completeLinearOrder : CompleteLinearOrder PUnit.{u_1 + 1}

@[simp]

theorem PUnit.sSup_eq (s : Set PUnit.{u + 1} ) : sSup s = PUnit.unit

@[simp]

theorem PUnit.sInf_eq (s : Set PUnit.{u + 1} ) : sInf s = PUnit.unit