English
In a complete lattice, IsAtomistic is equivalent to every element being a sup of atoms.
Русский
В полной решетке атомистичность эквивалентна тому, что каждый элемент является sup атомов.
LaTeX
$$nonrec theorem isAtomistic_iff {\\alpha} [CompleteLattice \\alpha] : IsAtomistic \\alpha \\iff \\forall b : \\alpha, \\exists s : Set \\alpha, b = sSup s ∧ \\forall a ∈ s, IsAtom a$$
Lean4
nonrec theorem isAtomistic_iff {α} [CompleteLattice α] :
IsAtomistic α ↔ ∀ b : α, ∃ s : Set α, b = sSup s ∧ ∀ a ∈ s, IsAtom a := by
simp_rw [isAtomistic_iff, isLUB_iff_sSup_eq, eq_comm]