English
At every stage i, the cardinality of generateMeasurableRec(s,i) does not exceed max(|s|, 2^{ℵ0}).
Русский
На каждой стадии i множество generateMeasurableRec(s,i) имеет кардинальность не более max(|s|, 2^{ℵ0}).
LaTeX
$$$\\#\\big(\\mathrm{generateMeasurableRec}(s,i)\\big) \\le \\max\\big(\\#s, 2^{\\aleph_0}\\big)$$$
Lean4
/-- At each step of the inductive construction, the cardinality bound `≤ #s ^ ℵ₀` holds. -/
theorem cardinal_generateMeasurableRec_le (s : Set (Set α)) (i : Ordinal.{v}) :
#(generateMeasurableRec s i) ≤ max (#s) 2 ^ ℵ₀ :=
by
suffices ∀ i ≤ ω₁, #(generateMeasurableRec s i) ≤ max (#s) 2 ^ ℵ₀
by
obtain hi | hi := le_or_gt i ω₁
· exact this i hi
· rw [generateMeasurableRec_of_omega1_le s hi.le]
exact this _ le_rfl
intro i
apply WellFoundedLT.induction i
intro i IH hi
have A : 𝔠 ≤ max (#s) 2 ^ ℵ₀ := power_le_power_right (le_max_right _ _)
have B := aleph0_le_continuum.trans A
have C : #(⋃ j < i, generateMeasurableRec s j) ≤ max (#s) 2 ^ ℵ₀ :=
by
apply mk_iUnion_Ordinal_lift_le_of_le _ B _
· intro j hj
exact IH j hj (hj.trans_le hi).le
· rw [lift_power, lift_aleph0]
rw [← Ordinal.lift_le.{u}, lift_omega, Ordinal.lift_one, ← ord_aleph] at hi
have H := card_le_of_le_ord hi
rw [← Ordinal.lift_card] at H
apply H.trans <| aleph_one_le_continuum.trans <| power_le_power_right _
rw [lift_max, Cardinal.lift_ofNat]
exact le_max_right _ _
rw [generateMeasurableRec]
apply_rules [(mk_union_le _ _).trans, add_le_of_le (aleph_one_le_continuum.trans A), mk_image_le.trans]
· exact (self_le_power _ one_le_aleph0).trans (power_le_power_right (le_max_left _ _))
· rw [mk_singleton]
exact one_lt_aleph0.le.trans B
· apply mk_range_le.trans
simp only [mk_pi, prod_const, Cardinal.lift_uzero, mk_denumerable, lift_aleph0]
have := @power_le_power_right _ _ ℵ₀ C
rwa [← power_mul, aleph0_mul_aleph0] at this
