English
The generated sigma-algebra at ω1 equals the union over i<ω1 of generateMeasurableRec s i.
Русский
Порождённая сигма-алгебра на ω1 равна объединению по i<ω1 generateMeasurableRec s i.
LaTeX
$$$\\mathrm{generateMeasurableRec}(s, \\omega_1) = \\bigcup_{i < \\omega_1} \\mathrm{generateMeasurableRec}(s,i)$$$
Lean4
theorem generateMeasurableRec_omega1 (s : Set (Set α)) :
generateMeasurableRec s (ω₁ : Ordinal.{v}) = ⋃ i < (ω₁ : Ordinal.{v}), generateMeasurableRec s i :=
by
apply (iUnion₂_subset fun i h => generateMeasurableRec_mono s h.le).antisymm'
intro t ht
rw [mem_iUnion₂]
refine generateMeasurableRec_induction ?_ ?_ ?_ ?_ ht
· intro t ht
exact ⟨0, omega_pos 1, self_subset_generateMeasurableRec s 0 ht⟩
· exact ⟨0, omega_pos 1, empty_mem_generateMeasurableRec s 0⟩
· rintro u - ⟨j, hj, hj'⟩
exact ⟨_, (isSuccLimit_omega 1).succ_lt hj, compl_mem_generateMeasurableRec (Order.lt_succ j) hj'⟩
· intro f H
choose I hI using fun n => (H n).1
simp_rw [exists_prop] at hI
refine
⟨_, Ordinal.lsub_lt_ord_lift ?_ fun n => (hI n).1,
iUnion_mem_generateMeasurableRec fun n => ⟨_, Ordinal.lt_lsub I n, (hI n).2⟩⟩
rw [mk_nat, lift_aleph0, isRegular_aleph_one.cof_omega_eq]
exact aleph0_lt_aleph_one
