English
countablePartition α n is a partition of α into at most 2^n sets; as n grows, partitions refine previous ones; the union over n generates the whole sigma-algebra.
Русский
countablePartition α n есть разбиение α на не более чем 2^n множества; с увеличением n разбиения уточняются; объединение по всем n порождает всю сигма-алгебру.
LaTeX
$$$\text{countablePartition}(\alpha)\, n \subseteq \text{Set}(\alpha)\quad\text{(partition properties and refinement statements)}$$$
Lean4
/-- For each `n : ℕ`, `countablePartition α n` is a partition of the space in at most
`2^n` sets. Each partition is finer than the preceding one. The measurable space generated by
the union of all those partitions is the measurable space on `α`. -/
def countablePartition (α : Type*) [MeasurableSpace α] [CountablyGenerated α] : ℕ → Set (Set α) :=
memPartition (enumerateCountable countable_countableGeneratingSet ∅)
