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.MinimalAxioms (α : Type u) extends CompleteLattice α : Type u

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.

• le : α → α → Prop
• lt : α → α → Prop
• le_refl (a : α) : a ≤ a
• le_trans (a b c : α) : a ≤ b → b ≤ c → a ≤ c
• lt_iff_le_not_ge (a b : α) : a < b ↔ a ≤ b ∧ ¬b ≤ a
• le_antisymm (a b : α) : a ≤ b → b ≤ a → a = b
• sup : α → α → α
• le_sup_left (a b : α) : a ≤ sup a b
• le_sup_right (a b : α) : b ≤ sup a b
• sup_le (a b c : α) : a ≤ c → b ≤ c → sup a b ≤ c
• inf : α → α → α
• inf_le_left (a b : α) : Lattice.inf a b ≤ a
• inf_le_right (a b : α) : Lattice.inf a b ≤ b
• le_inf (a b c : α) : a ≤ b → a ≤ c → a ≤ Lattice.inf b c
• sSup : Set α → α
• le_sSup (s : Set α) (a : α) : a ∈ s → a ≤ sSup s
• sSup_le (s : Set α) (a : α) : (∀ b ∈ s, b ≤ a) → sSup s ≤ a
• sInf : Set α → α
• sInf_le (s : Set α) (a : α) : a ∈ s → sInf s ≤ a
• le_sInf (s : Set α) (a : α) : (∀ b ∈ s, a ≤ b) → a ≤ sInf s
• top : α
• le_top (a : α) : a ≤ ⊤
• bot : α
• bot_le (a : α) : ⊥ ≤ a
• inf_sSup_le_iSup_inf (a : α) (s : Set α) : a ⊓ sSup s ≤ ⨆ b ∈ s, a ⊓ b

class Order.Coframe.MinimalAxioms (α : Type u) extends CompleteLattice α : Type u

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.

• le : α → α → Prop
• lt : α → α → Prop
• le_refl (a : α) : a ≤ a
• le_trans (a b c : α) : a ≤ b → b ≤ c → a ≤ c
• lt_iff_le_not_ge (a b : α) : a < b ↔ a ≤ b ∧ ¬b ≤ a
• le_antisymm (a b : α) : a ≤ b → b ≤ a → a = b
• sup : α → α → α
• le_sup_left (a b : α) : a ≤ sup a b
• le_sup_right (a b : α) : b ≤ sup a b
• sup_le (a b c : α) : a ≤ c → b ≤ c → sup a b ≤ c
• inf : α → α → α
• inf_le_left (a b : α) : Lattice.inf a b ≤ a
• inf_le_right (a b : α) : Lattice.inf a b ≤ b
• le_inf (a b c : α) : a ≤ b → a ≤ c → a ≤ Lattice.inf b c
• sSup : Set α → α
• le_sSup (s : Set α) (a : α) : a ∈ s → a ≤ sSup s
• sSup_le (s : Set α) (a : α) : (∀ b ∈ s, b ≤ a) → sSup s ≤ a
• sInf : Set α → α
• sInf_le (s : Set α) (a : α) : a ∈ s → sInf s ≤ a
• le_sInf (s : Set α) (a : α) : (∀ b ∈ s, a ≤ b) → a ≤ sInf s
• top : α
• le_top (a : α) : a ≤ ⊤
• bot : α
• bot_le (a : α) : ⊥ ≤ a
• iInf_sup_le_sup_sInf (a : α) (s : Set α) : ⨅ b ∈ s, a ⊔ b ≤ a ⊔ sInf s

class Order.Frame (α : Type u_1) extends CompleteLattice α, HeytingAlgebra α : Type u_1

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

• le : α → α → Prop
• lt : α → α → Prop
• le_refl (a : α) : a ≤ a
• le_trans (a b c : α) : a ≤ b → b ≤ c → a ≤ c
• lt_iff_le_not_ge (a b : α) : a < b ↔ a ≤ b ∧ ¬b ≤ a
• le_antisymm (a b : α) : a ≤ b → b ≤ a → a = b
• sup : α → α → α
• le_sup_left (a b : α) : a ≤ sup a b
• le_sup_right (a b : α) : b ≤ sup a b
• sup_le (a b c : α) : a ≤ c → b ≤ c → sup a b ≤ c
• inf : α → α → α
• inf_le_left (a b : α) : Lattice.inf a b ≤ a
• inf_le_right (a b : α) : Lattice.inf a b ≤ b
• le_inf (a b c : α) : a ≤ b → a ≤ c → a ≤ Lattice.inf b c
• sSup : Set α → α
• le_sSup (s : Set α) (a : α) : a ∈ s → a ≤ sSup s
• sSup_le (s : Set α) (a : α) : (∀ b ∈ s, b ≤ a) → sSup s ≤ a
• sInf : Set α → α
• sInf_le (s : Set α) (a : α) : a ∈ s → sInf s ≤ a
• le_sInf (s : Set α) (a : α) : (∀ b ∈ s, a ≤ b) → a ≤ sInf s
• top : α
• le_top (a : α) : a ≤ ⊤
• bot : α
• bot_le (a : α) : ⊥ ≤ a
• himp : α → α → α
• le_himp_iff (a b c : α) : a ≤ b ⇨ c ↔ a ⊓ b ≤ c
• compl : α → α
• himp_bot (a : α) : a ⇨ ⊥ = aᶜ

theorem inf_sSup_eq {α : Type u_1} [Order.Frame α] {s : Set α} {a : α} : a ⊓ sSup s = ⨆ b ∈ s, a ⊓ b

⊓ distributes over ⨆.

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

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

• le : α → α → Prop
• lt : α → α → Prop
• le_refl (a : α) : a ≤ a
• le_trans (a b c : α) : a ≤ b → b ≤ c → a ≤ c
• lt_iff_le_not_ge (a b : α) : a < b ↔ a ≤ b ∧ ¬b ≤ a
• le_antisymm (a b : α) : a ≤ b → b ≤ a → a = b
• sup : α → α → α
• le_sup_left (a b : α) : a ≤ sup a b
• le_sup_right (a b : α) : b ≤ sup a b
• sup_le (a b c : α) : a ≤ c → b ≤ c → sup a b ≤ c
• inf : α → α → α
• inf_le_left (a b : α) : Lattice.inf a b ≤ a
• inf_le_right (a b : α) : Lattice.inf a b ≤ b
• le_inf (a b c : α) : a ≤ b → a ≤ c → a ≤ Lattice.inf b c
• sSup : Set α → α
• le_sSup (s : Set α) (a : α) : a ∈ s → a ≤ sSup s
• sSup_le (s : Set α) (a : α) : (∀ b ∈ s, b ≤ a) → sSup s ≤ a
• sInf : Set α → α
• sInf_le (s : Set α) (a : α) : a ∈ s → sInf s ≤ a
• le_sInf (s : Set α) (a : α) : (∀ b ∈ s, a ≤ b) → a ≤ sInf s
• top : α
• le_top (a : α) : a ≤ ⊤
• bot : α
• bot_le (a : α) : ⊥ ≤ a
• sdiff : α → α → α
• sdiff_le_iff (a b c : α) : a \ b ≤ c ↔ a ≤ b ⊔ c
• hnot : α → α
• top_sdiff (a : α) : ⊤ \ a = ￢a

theorem sup_sInf_eq {α : Type u_1} [Order.Coframe α] {s : Set α} {a : α} : a ⊔ sInf s = ⨅ b ∈ s, a ⊔ b

⊔ distributes over ⨅.

structure CompleteDistribLattice.MinimalAxioms (α : Type u) extends CompleteLattice α, Order.Frame.MinimalAxioms α, Order.Coframe.MinimalAxioms α : Type u

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.

• le : α → α → Prop
• lt : α → α → Prop
• le_refl (a : α) : a ≤ a
• le_trans (a b c : α) : a ≤ b → b ≤ c → a ≤ c
• lt_iff_le_not_ge (a b : α) : a < b ↔ a ≤ b ∧ ¬b ≤ a
• le_antisymm (a b : α) : a ≤ b → b ≤ a → a = b
• sup : α → α → α
• le_sup_left (a b : α) : a ≤ sup a b
• le_sup_right (a b : α) : b ≤ sup a b
• sup_le (a b c : α) : a ≤ c → b ≤ c → sup a b ≤ c
• inf : α → α → α
• inf_le_left (a b : α) : Lattice.inf a b ≤ a
• inf_le_right (a b : α) : Lattice.inf a b ≤ b
• le_inf (a b c : α) : a ≤ b → a ≤ c → a ≤ Lattice.inf b c
• sSup : Set α → α
• le_sSup (s : Set α) (a : α) : a ∈ s → a ≤ sSup s
• sSup_le (s : Set α) (a : α) : (∀ b ∈ s, b ≤ a) → sSup s ≤ a
• sInf : Set α → α
• sInf_le (s : Set α) (a : α) : a ∈ s → sInf s ≤ a
• le_sInf (s : Set α) (a : α) : (∀ b ∈ s, a ≤ b) → a ≤ sInf s
• top : α
• le_top (a : α) : a ≤ ⊤
• bot : α
• bot_le (a : α) : ⊥ ≤ a
• inf_sSup_le_iSup_inf (a : α) (s : Set α) : a ⊓ sSup s ≤ ⨆ b ∈ s, a ⊓ b
• iInf_sup_le_sup_sInf (a : α) (s : Set α) : ⨅ b ∈ s, a ⊔ b ≤ a ⊔ sInf s

class CompleteDistribLattice (α : Type u_1) extends Order.Frame α, Order.Coframe α, BiheytingAlgebra α : Type u_1

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

• le : α → α → Prop
• lt : α → α → Prop
• le_refl (a : α) : a ≤ a
• le_trans (a b c : α) : a ≤ b → b ≤ c → a ≤ c
• lt_iff_le_not_ge (a b : α) : a < b ↔ a ≤ b ∧ ¬b ≤ a
• le_antisymm (a b : α) : a ≤ b → b ≤ a → a = b
• sup : α → α → α
• le_sup_left (a b : α) : a ≤ sup a b
• le_sup_right (a b : α) : b ≤ sup a b
• sup_le (a b c : α) : a ≤ c → b ≤ c → sup a b ≤ c
• inf : α → α → α
• inf_le_left (a b : α) : Lattice.inf a b ≤ a
• inf_le_right (a b : α) : Lattice.inf a b ≤ b
• le_inf (a b c : α) : a ≤ b → a ≤ c → a ≤ Lattice.inf b c
• sSup : Set α → α
• le_sSup (s : Set α) (a : α) : a ∈ s → a ≤ sSup s
• sSup_le (s : Set α) (a : α) : (∀ b ∈ s, b ≤ a) → sSup s ≤ a
• sInf : Set α → α
• sInf_le (s : Set α) (a : α) : a ∈ s → sInf s ≤ a
• le_sInf (s : Set α) (a : α) : (∀ b ∈ s, a ≤ b) → a ≤ sInf s
• top : α
• le_top (a : α) : a ≤ ⊤
• bot : α
• bot_le (a : α) : ⊥ ≤ a
• himp : α → α → α
• le_himp_iff (a b c : α) : a ≤ b ⇨ c ↔ a ⊓ b ≤ c
• compl : α → α
• himp_bot (a : α) : a ⇨ ⊥ = aᶜ
• sdiff : α → α → α
• sdiff_le_iff (a b c : α) : a \ b ≤ c ↔ a ≤ b ⊔ c
• hnot : α → α
• top_sdiff (a : α) : ⊤ \ a = ￢a

structure CompletelyDistribLattice.MinimalAxioms (α : Type u) extends CompleteLattice α : Type u

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.

• le : α → α → Prop
• lt : α → α → Prop
• le_refl (a : α) : a ≤ a
• le_trans (a b c : α) : a ≤ b → b ≤ c → a ≤ c
• lt_iff_le_not_ge (a b : α) : a < b ↔ a ≤ b ∧ ¬b ≤ a
• le_antisymm (a b : α) : a ≤ b → b ≤ a → a = b
• sup : α → α → α
• le_sup_left (a b : α) : a ≤ sup a b
• le_sup_right (a b : α) : b ≤ sup a b
• sup_le (a b c : α) : a ≤ c → b ≤ c → sup a b ≤ c
• inf : α → α → α
• inf_le_left (a b : α) : Lattice.inf a b ≤ a
• inf_le_right (a b : α) : Lattice.inf a b ≤ b
• le_inf (a b c : α) : a ≤ b → a ≤ c → a ≤ Lattice.inf b c
• sSup : Set α → α
• le_sSup (s : Set α) (a : α) : a ∈ s → a ≤ sSup s
• sSup_le (s : Set α) (a : α) : (∀ b ∈ s, b ≤ a) → sSup s ≤ a
• sInf : Set α → α
• sInf_le (s : Set α) (a : α) : a ∈ s → sInf s ≤ a
• le_sInf (s : Set α) (a : α) : (∀ b ∈ s, a ≤ b) → a ≤ sInf s
• top : α
• le_top (a : α) : a ≤ ⊤
• bot : α
• bot_le (a : α) : ⊥ ≤ a
• iInf_iSup_eq {ι : Type u} {κ : ι → Type u} (f : (a : ι) → κ a → α) : ⨅ (a : ι), ⨆ (b : κ a), f a b = ⨆ (g : (a : ι) → κ a), ⨅ (a : ι), f a (g a)

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

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

• le : α → α → Prop
• lt : α → α → Prop
• le_refl (a : α) : a ≤ a
• le_trans (a b c : α) : a ≤ b → b ≤ c → a ≤ c
• lt_iff_le_not_ge (a b : α) : a < b ↔ a ≤ b ∧ ¬b ≤ a
• le_antisymm (a b : α) : a ≤ b → b ≤ a → a = b
• sup : α → α → α
• le_sup_left (a b : α) : a ≤ sup a b
• le_sup_right (a b : α) : b ≤ sup a b
• sup_le (a b c : α) : a ≤ c → b ≤ c → sup a b ≤ c
• inf : α → α → α
• inf_le_left (a b : α) : Lattice.inf a b ≤ a
• inf_le_right (a b : α) : Lattice.inf a b ≤ b
• le_inf (a b c : α) : a ≤ b → a ≤ c → a ≤ Lattice.inf b c
• sSup : Set α → α
• le_sSup (s : Set α) (a : α) : a ∈ s → a ≤ sSup s
• sSup_le (s : Set α) (a : α) : (∀ b ∈ s, b ≤ a) → sSup s ≤ a
• sInf : Set α → α
• sInf_le (s : Set α) (a : α) : a ∈ s → sInf s ≤ a
• le_sInf (s : Set α) (a : α) : (∀ b ∈ s, a ≤ b) → a ≤ sInf s
• top : α
• le_top (a : α) : a ≤ ⊤
• bot : α
• bot_le (a : α) : ⊥ ≤ a
• himp : α → α → α
• le_himp_iff (a b c : α) : a ≤ b ⇨ c ↔ a ⊓ b ≤ c
• compl : α → α
• himp_bot (a : α) : a ⇨ ⊥ = aᶜ
• sdiff : α → α → α
• hnot : α → α
• sdiff_le_iff (a b c : α) : a \ b ≤ c ↔ a ≤ b ⊔ c
• top_sdiff (a : α) : ⊤ \ a = ￢a
• iInf_iSup_eq {ι : Type u} {κ : ι → Type u} (f : (a : ι) → κ a → α) : ⨅ (a : ι), ⨆ (b : κ a), f a b = ⨆ (g : (a : ι) → κ a), ⨅ (a : ι), f a (g a)

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 : MinimalAxioms α) {s : Set α} {a : α} : a ⊓ sSup s = ⨆ b ∈ s, a ⊓ b

theorem Order.Frame.MinimalAxioms.sSup_inf_eq {α : Type u} (minAx : MinimalAxioms α) {s : Set α} {b : α} : sSup s ⊓ b = ⨆ a ∈ s, a ⊓ b

theorem Order.Frame.MinimalAxioms.iSup_inf_eq {α : Type u} {ι : Sort w} (minAx : MinimalAxioms α) (f : ι → α) (a : α) : (⨆ (i : ι), f i) ⊓ a = ⨆ (i : ι), f i ⊓ a

theorem Order.Frame.MinimalAxioms.inf_iSup_eq {α : Type u} {ι : Sort w} (minAx : 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 : MinimalAxioms α) {f : (i : ι) → κ i → α} (a : α) : a ⊓ ⨆ (i : ι), ⨆ (j : κ i), f i j = ⨆ (i : ι), ⨆ (j : κ i), a ⊓ f i j

def Order.Frame.MinimalAxioms.of {α : Type u} [Frame α] : MinimalAxioms α

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

Equations

• Order.Frame.MinimalAxioms.of = { toCompleteLattice := inst✝.toCompleteLattice, inf_sSup_le_iSup_inf := ⋯ }

@[reducible, inline]

abbrev Order.Frame.ofMinimalAxioms {α : Type u} (minAx : MinimalAxioms α) : Frame α

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

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

Equations

• One or more equations did not get rendered due to their size.

theorem Order.Coframe.MinimalAxioms.sup_sInf_eq {α : Type u} (minAx : MinimalAxioms α) {s : Set α} {a : α} : a ⊔ sInf s = ⨅ b ∈ s, a ⊔ b

theorem Order.Coframe.MinimalAxioms.sInf_sup_eq {α : Type u} (minAx : MinimalAxioms α) {s : Set α} {b : α} : sInf s ⊔ b = ⨅ a ∈ s, a ⊔ b

theorem Order.Coframe.MinimalAxioms.iInf_sup_eq {α : Type u} {ι : Sort w} (minAx : MinimalAxioms α) (f : ι → α) (a : α) : (⨅ (i : ι), f i) ⊔ a = ⨅ (i : ι), f i ⊔ a

theorem Order.Coframe.MinimalAxioms.sup_iInf_eq {α : Type u} {ι : Sort w} (minAx : 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 : MinimalAxioms α) {f : (i : ι) → κ i → α} (a : α) : a ⊔ ⨅ (i : ι), ⨅ (j : κ i), f i j = ⨅ (i : ι), ⨅ (j : κ i), a ⊔ f i j

def Order.Coframe.MinimalAxioms.of {α : Type u} [Coframe α] : MinimalAxioms α

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

Equations

• Order.Coframe.MinimalAxioms.of = { toCompleteLattice := inst✝.toCompleteLattice, iInf_sup_le_sup_sInf := ⋯ }

@[reducible, inline]

abbrev Order.Coframe.ofMinimalAxioms {α : Type u} (minAx : MinimalAxioms α) : Coframe α

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

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

Equations

• One or more equations did not get rendered due to their size.

def CompleteDistribLattice.MinimalAxioms.of {α : Type u} [CompleteDistribLattice α] : MinimalAxioms α

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

Equations

• CompleteDistribLattice.MinimalAxioms.of = { toCompleteLattice := inst✝.toCompleteLattice, inf_sSup_le_iSup_inf := ⋯, iInf_sup_le_sup_sInf := ⋯ }

@[reducible, inline]

abbrev CompleteDistribLattice.MinimalAxioms.toFrame {α : Type u} (minAx : MinimalAxioms α) : Order.Frame.MinimalAxioms α

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

Equations

• minAx.toFrame = minAx.toFrameMinimalAxioms

@[reducible, inline]

abbrev CompleteDistribLattice.MinimalAxioms.toCoframe {α : Type u} (minAx : MinimalAxioms α) : Order.Coframe.MinimalAxioms α

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

Equations

• minAx.toCoframe = { toCompleteLattice := minAx.toCompleteLattice, iInf_sup_le_sup_sInf := ⋯ }

@[reducible, inline]

abbrev CompleteDistribLattice.ofMinimalAxioms {α : Type u} (minAx : MinimalAxioms α) : CompleteDistribLattice α

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

• One or more equations did not get rendered due to their size.

theorem CompletelyDistribLattice.MinimalAxioms.iInf_iSup_eq' {α : Type u} {ι : Sort w} {κ : ι → Sort w'} (minAx : MinimalAxioms α) (f : (a : ι) → κ a → α) : have 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 : MinimalAxioms α) (f : (i : ι) → κ i → α) : have x := minAx.toCompleteLattice; ⨆ (i : ι), ⨅ (j : κ i), f i j = ⨅ (g : (i : ι) → κ i), ⨆ (i : ι), f i (g i)

@[reducible, inline]

abbrev CompletelyDistribLattice.MinimalAxioms.toCompleteDistribLattice {α : Type u} (minAx : MinimalAxioms α) : CompleteDistribLattice.MinimalAxioms α

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 := ⋯ }

def CompletelyDistribLattice.MinimalAxioms.of {α : Type u} [CompletelyDistribLattice α] : MinimalAxioms α

The CompletelyDistribLattice.MinimalAxioms element corresponding to a frame.

Equations

• CompletelyDistribLattice.MinimalAxioms.of = { toCompleteLattice := inst✝.toCompleteLattice, iInf_iSup_eq := ⋯ }

@[reducible, inline]

abbrev CompletelyDistribLattice.ofMinimalAxioms {α : Type u} (minAx : MinimalAxioms α) : CompletelyDistribLattice α

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

• One or more equations did not get rendered due to their size.

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]

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

Equations

• One or more equations did not get rendered due to their size.

@[instance 100]

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.

theorem sSup_inf_eq {α : Type u} [Order.Frame α] {s : Set α} {b : α} : sSup s ⊓ b = ⨆ 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

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 ι'} : (⨆ i ∈ s, f i) ⊓ ⨆ j ∈ t, g j = ⨆ p ∈ s ×ˢ t, f p.1 ⊓ g p.2

theorem sSup_inf_sSup {α : Type u} [Order.Frame α] {s t : Set α} : sSup s ⊓ sSup t = ⨆ p ∈ s ×ˢ 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 ↔ ∀ b ∈ s, Disjoint b a

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

theorem himp_eq_sSup {α : Type u} [Order.Frame α] {a b : α} : a ⇨ b = sSup {w : α | w ⊓ a ≤ b}

theorem compl_eq_sSup_disjoint {α : Type u} [Order.Frame α] {a : α} : aᶜ = sSup {w : α | Disjoint w a}

theorem himp_le_iff {α : Type u} [Order.Frame α] {a b c : α} : a ⇨ b ≤ c ↔ ∀ (d : α), d ⊓ a ≤ b → d ≤ c

@[instance 100]

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

Equations

• Frame.toDistribLattice = DistribLattice.ofInfSupLe ⋯

instance Prod.instFrame {α : Type u} {β : Type v} [Order.Frame α] [Order.Frame β] : Order.Frame (α × β)

Equations

• Prod.instFrame = { toCompleteLattice := Prod.instCompleteLattice, toHImp := Prod.instHeytingAlgebra.toHImp, le_himp_iff := ⋯, toHasCompl := Prod.instHeytingAlgebra.toHasCompl, himp_bot := ⋯ }

instance Pi.instFrame {ι : Type u_1} {π : ι → Type u_2} [(i : ι) → Order.Frame (π i)] : Order.Frame ((i : ι) → π i)

Equations

• Pi.instFrame = { toCompleteLattice := Pi.instCompleteLattice, toHImp := Pi.instHeytingAlgebra.toHImp, le_himp_iff := ⋯, toHasCompl := Pi.instHeytingAlgebra.toHasCompl, himp_bot := ⋯ }

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

Equations

• One or more equations did not get rendered due to their size.

theorem sInf_sup_eq {α : Type u} [Order.Coframe α] {s : Set α} {b : α} : sInf s ⊔ b = ⨅ 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

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 ι'} : (⨅ i ∈ s, f i) ⊔ ⨅ j ∈ t, g j = ⨅ p ∈ s ×ˢ t, f p.1 ⊔ g p.2

theorem sInf_sup_sInf {α : Type u} [Order.Coframe α] {s t : Set α} : sInf s ⊔ sInf t = ⨅ p ∈ s ×ˢ 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

theorem sdiff_eq_sInf {α : Type u} [Order.Coframe α] {a b : α} : a \ b = sInf {w : α | a ≤ b ⊔ w}

theorem hnot_eq_sInf_codisjoint {α : Type u} [Order.Coframe α] {a : α} : ￢a = sInf {w : α | Codisjoint a w}

theorem le_sdiff_iff {α : Type u} [Order.Coframe α] {a b c : α} : a ≤ b \ c ↔ ∀ (d : α), b ≤ c ⊔ d → a ≤ d

@[instance 100]

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

Equations

• Coframe.toDistribLattice = { toLattice := inst✝.toLattice, le_sup_inf := ⋯ }

instance Prod.instCoframe {α : Type u} {β : Type v} [Order.Coframe α] [Order.Coframe β] : Order.Coframe (α × β)

Equations

• Prod.instCoframe = { toCompleteLattice := Prod.instCompleteLattice, toSDiff := Prod.instCoheytingAlgebra.toSDiff, sdiff_le_iff := ⋯, toHNot := Prod.instCoheytingAlgebra.toHNot, top_sdiff := ⋯ }

instance Pi.instCoframe {ι : Type u_1} {π : ι → Type u_2} [(i : ι) → Order.Coframe (π i)] : Order.Coframe ((i : ι) → π i)

Equations

• Pi.instCoframe = { toCompleteLattice := Pi.instCompleteLattice, toSDiff := Pi.instCoheytingAlgebra.toSDiff, sdiff_le_iff := ⋯, toHNot := Pi.instCoheytingAlgebra.toHNot, top_sdiff := ⋯ }

instance OrderDual.instCompleteDistribLattice {α : Type u} [CompleteDistribLattice α] : CompleteDistribLattice αᵒᵈ

Equations

• OrderDual.instCompleteDistribLattice = { toFrame := OrderDual.instFrame, toSDiff := OrderDual.instCoframe.toSDiff, sdiff_le_iff := ⋯, toHNot := OrderDual.instCoframe.toHNot, top_sdiff := ⋯ }

instance Prod.instCompleteDistribLattice {α : Type u} {β : Type v} [CompleteDistribLattice α] [CompleteDistribLattice β] : CompleteDistribLattice (α × β)

Equations

• Prod.instCompleteDistribLattice = { toFrame := Prod.instFrame, toSDiff := Prod.instCoframe.toSDiff, sdiff_le_iff := ⋯, toHNot := Prod.instCoframe.toHNot, top_sdiff := ⋯ }

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

Equations

• Pi.instCompleteDistribLattice = { toFrame := Pi.instFrame, toSDiff := Pi.instCoframe.toSDiff, sdiff_le_iff := ⋯, toHNot := Pi.instCoframe.toHNot, top_sdiff := ⋯ }

instance OrderDual.instCompletelyDistribLattice {α : Type u} [CompletelyDistribLattice α] : CompletelyDistribLattice αᵒᵈ

Equations

• One or more equations did not get rendered due to their size.

instance Prod.instCompletelyDistribLattice {α : Type u} {β : Type v} [CompletelyDistribLattice α] [CompletelyDistribLattice β] : CompletelyDistribLattice (α × β)

Equations

• One or more equations did not get rendered due to their size.

instance Pi.instCompletelyDistribLattice {ι : 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 CompleteLattice α, BooleanAlgebra α : Type u_1

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

It is only completely distributive if it is also atomic.

• le : α → α → Prop
• lt : α → α → Prop
• le_refl (a : α) : a ≤ a
• le_trans (a b c : α) : a ≤ b → b ≤ c → a ≤ c
• lt_iff_le_not_ge (a b : α) : a < b ↔ a ≤ b ∧ ¬b ≤ a
• le_antisymm (a b : α) : a ≤ b → b ≤ a → a = b
• sup : α → α → α
• le_sup_left (a b : α) : a ≤ sup a b
• le_sup_right (a b : α) : b ≤ sup a b
• sup_le (a b c : α) : a ≤ c → b ≤ c → sup a b ≤ c
• inf : α → α → α
• inf_le_left (a b : α) : Lattice.inf a b ≤ a
• inf_le_right (a b : α) : Lattice.inf a b ≤ b
• le_inf (a b c : α) : a ≤ b → a ≤ c → a ≤ Lattice.inf b c
• sSup : Set α → α
• le_sSup (s : Set α) (a : α) : a ∈ s → a ≤ sSup s
• sSup_le (s : Set α) (a : α) : (∀ b ∈ s, b ≤ a) → sSup s ≤ a
• sInf : Set α → α
• sInf_le (s : Set α) (a : α) : a ∈ s → sInf s ≤ a
• le_sInf (s : Set α) (a : α) : (∀ b ∈ s, a ≤ b) → a ≤ sInf s
• top : α
• le_top (a : α) : a ≤ ⊤
• bot : α
• bot_le (a : α) : ⊥ ≤ a
• le_sup_inf (x y z : α) : (x ⊔ y) ⊓ (x ⊔ z) ≤ x ⊔ y ⊓ z
• compl : α → α
• sdiff : α → α → α
• himp : α → α → α
• inf_compl_le_bot (x : α) : x ⊓ xᶜ ≤ ⊥
• top_le_sup_compl (x : α) : ⊤ ≤ x ⊔ xᶜ
• sdiff_eq (x y : α) : x \ y = x ⊓ yᶜ
• himp_eq (x y : α) : x ⇨ y = y ⊔ xᶜ

@[instance 100]

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

Equations

• One or more equations did not get rendered due to their size.

instance Prod.instCompleteBooleanAlgebra {α : Type u} {β : Type v} [CompleteBooleanAlgebra α] [CompleteBooleanAlgebra β] : CompleteBooleanAlgebra (α × β)

Equations

• One or more equations did not get rendered due to their size.

instance Pi.instCompleteBooleanAlgebra {ι : 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.

instance OrderDual.instCompleteBooleanAlgebra {α : Type u} [CompleteBooleanAlgebra α] : CompleteBooleanAlgebra αᵒᵈ

Equations

• One or more equations did not get rendered due to their size.

@[deprecated "use `inf_sSup_eq.le` instead" (since := "2025-06-15")]

theorem inf_sSup_le_iSup_inf {α : Type u} [CompleteBooleanAlgebra α] (a : α) (s : Set α) : a ⊓ sSup s ≤ ⨆ b ∈ s, a ⊓ b

@[deprecated "use `sup_sInf_eq.ge` instead" (since := "2025-06-15")]

theorem iInf_sup_le_sup_sInf {α : Type u} [CompleteBooleanAlgebra α] (a : α) (s : Set α) : ⨅ b ∈ s, a ⊔ b ≤ a ⊔ sInf s

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 ∈ s, iᶜ

theorem compl_sSup {α : Type u} [CompleteBooleanAlgebra α] {s : Set α} : (sSup s)ᶜ = ⨅ 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)

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

class CompleteAtomicBooleanAlgebra (α : Type u) extends CompleteBooleanAlgebra α : Type u

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.

• le : α → α → Prop
• lt : α → α → Prop
• le_refl (a : α) : a ≤ a
• le_trans (a b c : α) : a ≤ b → b ≤ c → a ≤ c
• lt_iff_le_not_ge (a b : α) : a < b ↔ a ≤ b ∧ ¬b ≤ a
• le_antisymm (a b : α) : a ≤ b → b ≤ a → a = b
• sup : α → α → α
• le_sup_left (a b : α) : a ≤ sup a b
• le_sup_right (a b : α) : b ≤ sup a b
• sup_le (a b c : α) : a ≤ c → b ≤ c → sup a b ≤ c
• inf : α → α → α
• inf_le_left (a b : α) : Lattice.inf a b ≤ a
• inf_le_right (a b : α) : Lattice.inf a b ≤ b
• le_inf (a b c : α) : a ≤ b → a ≤ c → a ≤ Lattice.inf b c
• sSup : Set α → α
• le_sSup (s : Set α) (a : α) : a ∈ s → a ≤ sSup s
• sSup_le (s : Set α) (a : α) : (∀ b ∈ s, b ≤ a) → sSup s ≤ a
• sInf : Set α → α
• sInf_le (s : Set α) (a : α) : a ∈ s → sInf s ≤ a
• le_sInf (s : Set α) (a : α) : (∀ b ∈ s, a ≤ b) → a ≤ sInf s
• top : α
• le_top (a : α) : a ≤ ⊤
• bot : α
• bot_le (a : α) : ⊥ ≤ a
• le_sup_inf (x y z : α) : (x ⊔ y) ⊓ (x ⊔ z) ≤ x ⊔ y ⊓ z
• compl : α → α
• sdiff : α → α → α
• himp : α → α → α
• inf_compl_le_bot (x : α) : x ⊓ xᶜ ≤ ⊥
• top_le_sup_compl (x : α) : ⊤ ≤ x ⊔ xᶜ
• sdiff_eq (x y : α) : x \ y = x ⊓ yᶜ
• himp_eq (x y : α) : x ⇨ y = y ⊔ xᶜ
• iInf_iSup_eq {ι : Type u} {κ : ι → Type u} (f : (a : ι) → κ a → α) : ⨅ (a : ι), ⨆ (b : κ a), f a b = ⨆ (g : (a : ι) → κ a), ⨅ (a : ι), f a (g a)

@[instance 100]

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

Equations

• One or more equations did not get rendered due to their size.

instance Prod.instCompleteAtomicBooleanAlgebra {α : Type u} {β : Type v} [CompleteAtomicBooleanAlgebra α] [CompleteAtomicBooleanAlgebra β] : CompleteAtomicBooleanAlgebra (α × β)

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• Pi.instCompleteAtomicBooleanAlgebra = { toCompleteBooleanAlgebra := Pi.instCompleteBooleanAlgebra, iInf_iSup_eq := ⋯ }

instance OrderDual.instCompleteAtomicBooleanAlgebra {α : Type u} [CompleteAtomicBooleanAlgebra α] : CompleteAtomicBooleanAlgebra αᵒᵈ

Equations

• OrderDual.instCompleteAtomicBooleanAlgebra = { toCompleteBooleanAlgebra := OrderDual.instCompleteBooleanAlgebra, iInf_iSup_eq := ⋯ }

instance Prop.instCompleteAtomicBooleanAlgebra : CompleteAtomicBooleanAlgebra Prop

Equations

• One or more equations did not get rendered due to their size.

instance Prop.instCompleteBooleanAlgebra : CompleteBooleanAlgebra Prop

Equations

• «Prop».instCompleteBooleanAlgebra = inferInstance

@[reducible, inline]

abbrev Function.Injective.frameMinimalAxioms {α : Type u} {β : Type v} [Max α] [Min α] [SupSet α] [InfSet α] [Top α] [Bot α] (minAx : Order.Frame.MinimalAxioms β) (f : α → β) (hf : 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 ∈ s, f a) (map_sInf : ∀ (s : Set α), f (sInf s) = ⨅ a ∈ s, f a) (map_top : f ⊤ = ⊤) (map_bot : f ⊥ = ⊥) : Order.Frame.MinimalAxioms α

Pullback an Order.Frame.MinimalAxioms along an injection.

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

abbrev Function.Injective.coframeMinimalAxioms {α : Type u} {β : Type v} [Max α] [Min α] [SupSet α] [InfSet α] [Top α] [Bot α] (minAx : Order.Coframe.MinimalAxioms β) (f : α → β) (hf : 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 ∈ s, f a) (map_sInf : ∀ (s : Set α), f (sInf s) = ⨅ a ∈ s, f a) (map_top : f ⊤ = ⊤) (map_bot : f ⊥ = ⊥) : Order.Coframe.MinimalAxioms α

Pullback an Order.Coframe.MinimalAxioms along an injection.

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

abbrev Function.Injective.frame {α : Type u} {β : Type v} [Max α] [Min α] [SupSet α] [InfSet α] [Top α] [Bot α] [HasCompl α] [HImp α] [Order.Frame β] (f : α → β) (hf : 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 ∈ s, f a) (map_sInf : ∀ (s : Set α), f (sInf s) = ⨅ a ∈ s, 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) : Order.Frame α

Pullback an Order.Frame along an injection.

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

abbrev Function.Injective.coframe {α : Type u} {β : Type v} [Max α] [Min α] [SupSet α] [InfSet α] [Top α] [Bot α] [HNot α] [SDiff α] [Order.Coframe β] (f : α → β) (hf : 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 ∈ s, f a) (map_sInf : ∀ (s : Set α), f (sInf s) = ⨅ a ∈ s, 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) : Order.Coframe α

Pullback an Order.Coframe along an injection.

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

abbrev Function.Injective.completeDistribLatticeMinimalAxioms {α : Type u} {β : Type v} [Max α] [Min α] [SupSet α] [InfSet α] [Top α] [Bot α] (minAx : CompleteDistribLattice.MinimalAxioms β) (f : α → β) (hf : Injective f) (map_sup : have x := minAx.toCompleteLattice; ∀ (a b : α), f (a ⊔ b) = f a ⊔ f b) (map_inf : have x := minAx.toCompleteLattice; ∀ (a b : α), f (a ⊓ b) = f a ⊓ f b) (map_sSup : have x := minAx.toCompleteLattice; ∀ (s : Set α), f (sSup s) = ⨆ a ∈ s, f a) (map_sInf : have x := minAx.toCompleteLattice; ∀ (s : Set α), f (sInf s) = ⨅ a ∈ s, f a) (map_top : have x := minAx.toCompleteLattice; f ⊤ = ⊤) (map_bot : have x := minAx.toCompleteLattice; f ⊥ = ⊥) : CompleteDistribLattice.MinimalAxioms α

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} [Max α] [Min α] [SupSet α] [InfSet α] [Top α] [Bot α] [HasCompl α] [HImp α] [HNot α] [SDiff α] [CompleteDistribLattice β] (f : α → β) (hf : 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 ∈ s, f a) (map_sInf : ∀ (s : Set α), f (sInf s) = ⨅ a ∈ s, 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) : CompleteDistribLattice α

Pullback a CompleteDistribLattice along an injection.

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

abbrev Function.Injective.completelyDistribLatticeMinimalAxioms {α : Type u} {β : Type v} [Max α] [Min α] [SupSet α] [InfSet α] [Top α] [Bot α] (minAx : CompletelyDistribLattice.MinimalAxioms β) (f : α → β) (hf : Injective f) (map_sup : have x := minAx.toCompleteLattice; ∀ (a b : α), f (a ⊔ b) = f a ⊔ f b) (map_inf : have x := minAx.toCompleteLattice; ∀ (a b : α), f (a ⊓ b) = f a ⊓ f b) (map_sSup : have x := minAx.toCompleteLattice; ∀ (s : Set α), f (sSup s) = ⨆ a ∈ s, f a) (map_sInf : have x := minAx.toCompleteLattice; ∀ (s : Set α), f (sInf s) = ⨅ a ∈ s, f a) (map_top : have x := minAx.toCompleteLattice; f ⊤ = ⊤) (map_bot : have x := minAx.toCompleteLattice; f ⊥ = ⊥) : CompletelyDistribLattice.MinimalAxioms α

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} [Max α] [Min α] [SupSet α] [InfSet α] [Top α] [Bot α] [HasCompl α] [HImp α] [HNot α] [SDiff α] [CompletelyDistribLattice β] (f : α → β) (hf : 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 ∈ s, f a) (map_sInf : ∀ (s : Set α), f (sInf s) = ⨅ a ∈ s, 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) : CompletelyDistribLattice α

Pullback a CompletelyDistribLattice along an injection.

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

abbrev Function.Injective.completeBooleanAlgebra {α : Type u} {β : Type v} [Max α] [Min α] [SupSet α] [InfSet α] [Top α] [Bot α] [HasCompl α] [HImp α] [SDiff α] [CompleteBooleanAlgebra β] (f : α → β) (hf : 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 ∈ s, f a) (map_sInf : ∀ (s : Set α), f (sInf s) = ⨅ a ∈ s, 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) : CompleteBooleanAlgebra α

Pullback a CompleteBooleanAlgebra along an injection.

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

abbrev Function.Injective.completeAtomicBooleanAlgebra {α : Type u} {β : Type v} [Max α] [Min α] [SupSet α] [InfSet α] [Top α] [Bot α] [HasCompl α] [HImp α] [HNot α] [SDiff α] [CompleteAtomicBooleanAlgebra β] (f : α → β) (hf : 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 ∈ s, f a) (map_sInf : ∀ (s : Set α), f (sInf s) = ⨅ a ∈ s, 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) : CompleteAtomicBooleanAlgebra α

Pullback a CompleteAtomicBooleanAlgebra along an injection.

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• PUnit.instCompleteBooleanAlgebra = inferInstance

@[simp]

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

@[simp]

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