English
There is a filtration of sigma-algebras indexed by natural numbers given by F_n = generatedFrom(memPartition t n) for all n, and this filtration is increasing in n, i.e., F_n ⊆ F_{n+1}.
Русский
Существует фильтрация сигм-алгебр, индексируемая по натуральным числам, такая что F_n = generateFrom(memPartition t n) для всех n, и она возрастает по n: F_n ⊆ F_{n+1}.
LaTeX
$$$$ \mathcal F_n = \operatorname{generateFrom}(\operatorname{memPartition}(t,n)) \quad (n \in \mathbb{N}), \quad \mathcal F_n \subseteq \mathcal F_{n+1} \; (\forall n). $$$$
Lean4
/-- A filtration built from the measurable spaces generated by the partitions `memPartition t n` for
all `n : ℕ`. -/
def partitionFiltration (ht : ∀ n, MeasurableSet (t n)) : Filtration ℕ m
where
seq n := generateFrom (memPartition t n)
mono' := monotone_nat_of_le_succ (generateFrom_memPartition_le_succ _)
le' := generateFrom_memPartition_le ht
