English
Let s be a collection of subsets of α. The sigma-algebra generated by s is exactly the ω1-th stage of the transfinite construction; i.e., the sets t that belong to the generated sigma-algebra are precisely the sets in the ω1-th iteration.
Русский
Пусть s — множество подмножеств множества α. Порождённая им σ‑алгебра совпадает с ω1-й стадией трансфинитной конструкции; то есть множество t принадлежит порождаемой σ‑алгебре тогда и только тогда, когда t находится на стадии ω1.
LaTeX
$$$\\{t \\subseteq \\alpha \\mid t \\in \\sigma(s)\\} = \\sigma_{\\omega_1}(s)$$$
Lean4
/-- `generateMeasurableRec s ω₁` generates precisely the smallest sigma-algebra containing `s`. -/
theorem generateMeasurable_eq_rec (s : Set (Set α)) : {t | GenerateMeasurable s t} = generateMeasurableRec s ω₁ :=
by
apply (generateMeasurableRec_subset s _).antisymm'
intro t ht
induction ht with
| basic u hu => exact self_subset_generateMeasurableRec s _ hu
| empty => exact empty_mem_generateMeasurableRec s _
| compl u _ IH =>
rw [generateMeasurableRec_omega1, mem_iUnion₂] at IH
obtain ⟨i, hi, hi'⟩ := IH
exact
generateMeasurableRec_mono _ ((isSuccLimit_omega 1).succ_lt hi).le
(compl_mem_generateMeasurableRec (Order.lt_succ i) hi')
| iUnion f _ IH =>
simp_rw [generateMeasurableRec_omega1, mem_iUnion₂, exists_prop] at IH
exact iUnion_mem_generateMeasurableRec IH
