mathlib documentation

order.complete_boolean_algebra

@[class]
structure complete_distrib_lattice (α : Type u_1) :
Type u_1

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.

Instances
theorem sup_Inf_eq {α : Type u} [complete_distrib_lattice α] {a : α} {s : set α} :
a Inf s = ⨅ (b : α) (H : b s), a b
theorem Inf_sup_eq {α : Type u} [complete_distrib_lattice α] {b : α} {s : set α} :
Inf s b = ⨅ (a : α) (H : a s), a b
theorem inf_Sup_eq {α : Type u} [complete_distrib_lattice α] {a : α} {s : set α} :
a Sup s = ⨆ (b : α) (H : b s), a b
theorem Sup_inf_eq {α : Type u} [complete_distrib_lattice α] {b : α} {s : set α} :
Sup s b = ⨆ (a : α) (H : a s), a b
theorem supr_inf_eq {α : Type u} {ι : Sort w} [complete_distrib_lattice α] (f : ι → α) (a : α) :
(⨆ (i : ι), f i) a = ⨆ (i : ι), f i a
theorem inf_supr_eq {α : Type u} {ι : Sort w} [complete_distrib_lattice α] (a : α) (f : ι → α) :
(a ⨆ (i : ι), f i) = ⨆ (i : ι), a f i
theorem infi_sup_eq {α : Type u} {ι : Sort w} [complete_distrib_lattice α] (f : ι → α) (a : α) :
(⨅ (i : ι), f i) a = ⨅ (i : ι), f i a
theorem sup_infi_eq {α : Type u} {ι : Sort w} [complete_distrib_lattice α] (a : α) (f : ι → α) :
(a ⨅ (i : ι), f i) = ⨅ (i : ι), a f i
theorem Inf_sup_Inf {α : Type u} [complete_distrib_lattice α] {s t : set α} :
Inf s Inf t = ⨅ (p : α × α) (H : p s.prod t), p.fst p.snd
theorem Sup_inf_Sup {α : Type u} [complete_distrib_lattice α] {s t : set α} :
Sup s Sup t = ⨆ (p : α × α) (H : p s.prod t), p.fst p.snd
theorem supr_disjoint_iff {α : Type u} {ι : Sort w} [complete_distrib_lattice α] {a : α} {f : ι → α} :
disjoint (⨆ (i : ι), f i) a ∀ (i : ι), disjoint (f i) a
theorem disjoint_supr_iff {α : Type u} {ι : Sort w} [complete_distrib_lattice α] {a : α} {f : ι → α} :
disjoint a (⨆ (i : ι), f i) ∀ (i : ι), disjoint a (f i)
@[class]
structure complete_boolean_algebra (α : Type u_1) :
Type u_1

A complete boolean algebra is a completely distributive boolean algebra.

Instances
theorem compl_infi {α : Type u} {ι : Sort w} [complete_boolean_algebra α] {f : ι → α} :
(infi f) = ⨆ (i : ι), (f i)
theorem compl_supr {α : Type u} {ι : Sort w} [complete_boolean_algebra α] {f : ι → α} :
(supr f) = ⨅ (i : ι), (f i)
theorem compl_Inf {α : Type u} [complete_boolean_algebra α] {s : set α} :
(Inf s) = ⨆ (i : α) (H : i s), i
theorem compl_Sup {α : Type u} [complete_boolean_algebra α] {s : set α} :
(Sup s) = ⨅ (i : α) (H : i s), i