English
In the lattice of all subsets of a type α (ordered by inclusion), an element s is an atom if and only if s is a singleton {x} for some x in α.
Русский
В решётке множестv подмножеств α, упорядоченной по включению, элемент s является атомом тогда и только тогда, когда s = {x} для некоторого x ∈ α.
LaTeX
$$$\\mathrm{IsAtom}(s) \\iff \\exists x, s = \\{x\\}$$$
Lean4
theorem isAtom_iff {s : Set α} : IsAtom s ↔ ∃ x, s = { x } :=
by
refine
⟨?_, by
rintro ⟨x, rfl⟩
exact isAtom_singleton x⟩
rw [isAtom_iff_le_of_ge, bot_eq_empty, ← nonempty_iff_ne_empty]
rintro ⟨⟨x, hx⟩, hs⟩
exact
⟨x,
eq_singleton_iff_unique_mem.2
⟨hx, fun y hy => (hs { y } (singleton_ne_empty _) (singleton_subset_iff.2 hy) hx).symm⟩⟩
