instIsAtomistic — Mathlib

English

The lattice of all subsets of α is atomistic: every subset s is the union of the atoms {a} for a ∈ s, i.e., s = ⋃_{a ∈ s} {a}.

Русский

Булева алгебра подмножеств α атомистическая: каждое множество s является объединением атомов {a} для a ∈ s, т.е. s = ⋃_{a ∈ s} {a}.

LaTeX

$$$s \\subseteq \\alpha \\to s = \\bigcup_{a \\in s} \\{a\\}$$$

Lean4

instance : IsAtomistic (Set α) :=
  inferInstance

Похожие утверждения