English
A collection of sets is countably spanning if there exists a countable sequence of sets from the collection whose union is the whole space.
Русский
Множество множеств счётно порождено, если существует счётная последовательность принадлежащих этому множеству, чья объединение равно всему пространству.
LaTeX
$$$\\mathrm{IsCountablySpanning}\\ (\\mathcal{C}) := \\exists s: \\mathbb{N} \\to \\mathcal{P}(\\alpha),\\ (\\forall n, s(n) \\in \\mathcal{C}) \\land \\bigcup_{n} s(n) = \\mathrm{univ}$$$
Lean4
/-- We say that a collection of sets is countably spanning if a countable subset spans the
whole type. This is a useful condition in various parts of measure theory. For example, it is
a needed condition to show that the product of two collections generate the product sigma algebra,
see `generateFrom_prod_eq`. -/
def IsCountablySpanning (C : Set (Set α)) : Prop :=
∃ s : ℕ → Set α, (∀ n, s n ∈ C) ∧ ⋃ n, s n = univ
