English
For a complete lattice with atomistic structure, every element b can be written as the supremum of a set of atoms.
Русский
В атомистичной полной решетке каждый элемент равен супремусу некоторого множества атомов.
LaTeX
$$∃ s : Set α, b = sSup s ∧ ∀ a ∈ s, IsAtom a$$
Lean4
theorem eq_sSup_atoms {α} [CompleteLattice α] [IsAtomistic α] (b : α) : ∃ s : Set α, b = sSup s ∧ ∀ a ∈ s, IsAtom a :=
CompleteLattice.isAtomistic_iff.1 ‹_› b