Theorems · Theorem · order theory

IsCompactlyGenerated.BooleanGenerators.finitelyAtomistic

∀ {α : Type u_1} [inst : CompleteLattice α] {S : Set α},
  IsCompactlyGenerated.BooleanGenerators S →
    ∀ (s : Finset α) (a : α), ↑s ⊆ S → IsCompactElement a → a ≤ s.sup id → ∃ t ⊆ s, a = t.sup id

The elements in a collection of Boolean generators satisfy 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.

Defined in

Mathlib.Order.BooleanGenerators

Cited by

2 results in Mathlib

Foundations

Depth 55 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CompleteLattice