Theorems · Inductive type · order theory

IsCompactlyGenerated.BooleanGenerators

{α : Type u_1} → [CompleteLattice α] → Set α → Prop

An alternative constructor for Boolean algebras. A set of Boolean generators in a compactly generated complete lattice is a subset S such that * the elements of S are all atoms, and * the set S satisfies an atomicity condition: any compact element below the supremum of a finite subset s of generators is equal to the supremum of a subset of s. If the supremum of S is the whole lattice, then the lattice is a Boolean algebra (see IsCompactlyGenerated.BooleanGenerators.booleanAlgebraOfSSupEqTop).

Defined in

Mathlib.Order.BooleanGenerators

Cited by

11 results in Mathlib

Foundations

Depth 1 from the axioms · uses no axioms

Assumes

CompleteLattice