mathlib documentation

• sup : α → α → α
• le : α → α → Prop
• lt : α → α → Prop
• le_refl : ∀ (a : α), a ≤ a
• le_trans : ∀ (a b c_1 : α), a ≤ b → b ≤ c_1 → a ≤ c_1
• lt_iff_le_not_le : (∀ (a b : α), a < b ↔ a ≤ b ∧ ¬b ≤ a) . "order_laws_tac"
• 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_1 : α), a ≤ c_1 → b ≤ c_1 → a ⊔ b ≤ c_1
• inf : α → α → α
• inf_le_left : ∀ (a b : α), a ⊓ b ≤ a
• inf_le_right : ∀ (a b : α), a ⊓ b ≤ b
• le_inf : ∀ (a b c_1 : α), a ≤ b → a ≤ c_1 → a ≤ b ⊓ c_1
• top : α
• le_top : ∀ (a : α), a ≤ ⊤
• bot : α
• bot_le : ∀ (a : α), ⊥ ≤ a
• Sup : set α → α
• Inf : set α → α
• le_Sup : ∀ (s : set α) (a : α), a ∈ s → a ≤ complete_distrib_lattice.Sup s
• Sup_le : ∀ (s : set α) (a : α), (∀ (b : α), b ∈ s → b ≤ a) → complete_distrib_lattice.Sup s ≤ a
• Inf_le : ∀ (s : set α) (a : α), a ∈ s → complete_distrib_lattice.Inf s ≤ a
• le_Inf : ∀ (s : set α) (a : α), (∀ (b : α), b ∈ s → a ≤ b) → a ≤ complete_distrib_lattice.Inf s
• infi_sup_le_sup_Inf : ∀ (a : α) (s : set α), (⨅ (b : α) (H : b ∈ s), a ⊔ b) ≤ a ⊔ complete_distrib_lattice.Inf s
• inf_Sup_le_supr_inf : ∀ (a : α) (s : set α), a ⊓ complete_distrib_lattice.Sup s ≤ ⨆ (b : α) (H : b ∈ s), a ⊓ b

A complete distributive lattice is a bit stronger than the name might suggest; perhaps completely distributive lattice is more descriptive, as this class includes a requirement that the lattice join distribute over arbitrary infima, and similarly for the dual.

• sup : α → α → α
• le : α → α → Prop
• lt : α → α → Prop
• le_refl : ∀ (a : α), a ≤ a
• le_trans : ∀ (a b c_1 : α), a ≤ b → b ≤ c_1 → a ≤ c_1
• lt_iff_le_not_le : (∀ (a b : α), a < b ↔ a ≤ b ∧ ¬b ≤ a) . "order_laws_tac"
• 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_1 : α), a ≤ c_1 → b ≤ c_1 → a ⊔ b ≤ c_1
• inf : α → α → α
• inf_le_left : ∀ (a b : α), a ⊓ b ≤ a
• inf_le_right : ∀ (a b : α), a ⊓ b ≤ b
• le_inf : ∀ (a b c_1 : α), a ≤ b → a ≤ c_1 → a ≤ b ⊓ c_1
• le_sup_inf : ∀ (x y z : α), (x ⊔ y) ⊓ (x ⊔ z) ≤ x ⊔ y ⊓ z
• top : α
• le_top : ∀ (a : α), a ≤ ⊤
• bot : α
• bot_le : ∀ (a : α), ⊥ ≤ a
• compl : α → α
• sdiff : α → α → α
• inf_compl_le_bot : ∀ (x : α), x ⊓ xᶜ ≤ ⊥
• top_le_sup_compl : ∀ (x : α), ⊤ ≤ x ⊔ xᶜ
• sdiff_eq : ∀ (x y : α), x \ y = x ⊓ yᶜ
• Sup : set α → α
• Inf : set α → α
• le_Sup : ∀ (s : set α) (a : α), a ∈ s → a ≤ complete_boolean_algebra.Sup s
• Sup_le : ∀ (s : set α) (a : α), (∀ (b : α), b ∈ s → b ≤ a) → complete_boolean_algebra.Sup s ≤ a
• Inf_le : ∀ (s : set α) (a : α), a ∈ s → complete_boolean_algebra.Inf s ≤ a
• le_Inf : ∀ (s : set α) (a : α), (∀ (b : α), b ∈ s → a ≤ b) → a ≤ complete_boolean_algebra.Inf s
• infi_sup_le_sup_Inf : ∀ (a : α) (s : set α), (⨅ (b : α) (H : b ∈ s), a ⊔ b) ≤ a ⊔ complete_boolean_algebra.Inf s
• inf_Sup_le_supr_inf : ∀ (a : α) (s : set α), a ⊓ complete_boolean_algebra.Sup s ≤ ⨆ (b : α) (H : b ∈ s), a ⊓ b

A complete boolean algebra is a completely distributive boolean algebra.