English
The sigma-algebra generated by the union over n of memPartition t n is equal to the sigma-algebra generated by the range of t.
Русский
Сигма-алгебра, порождаемая объединением по всем n разбиения memPartition t n, равна сигма-алгебре, порождаемой диапазоном t.
LaTeX
$$$\ generateFrom(\bigcup_{n} memPartition(t,n)) = \ generateFrom(\operatorname{range}(t)).$$$
Lean4
theorem generateFrom_iUnion_memPartition (t : ℕ → Set α) :
generateFrom (⋃ n, memPartition t n) = generateFrom (range t) :=
by
refine le_antisymm (generateFrom_le fun u hu ↦ ?_) (generateFrom_le fun u hu ↦ ?_)
· simp only [mem_iUnion] at hu
obtain ⟨n, hun⟩ := hu
induction n generalizing u with
| zero =>
simp only [memPartition_zero, mem_singleton_iff] at hun
rw [hun]
exact MeasurableSet.univ
| succ n ih =>
simp only [memPartition_succ, mem_setOf_eq] at hun
obtain ⟨v, hv, huv⟩ := hun
rcases huv with rfl | rfl
· exact (ih v hv).inter (measurableSet_generateFrom ⟨n, rfl⟩)
· exact (ih v hv).diff (measurableSet_generateFrom ⟨n, rfl⟩)
· simp only [mem_range] at hu
obtain ⟨n, rfl⟩ := hu
exact generateFrom_mono (subset_iUnion _ _) _ (measurableSet_generateFrom_memPartition t n)
