α : Type u
s : Set (Set α)
⊢ (#↑(⋃ (i : (Quotient.out (ord (aleph 1))).α), generateMeasurableRec s i)) ≤ max (#↑s) 2 ^ ℵ₀
α : Type u
s : Set (Set α)
⊢ (#↑{t | GenerateMeasurable s t}) ≤ max (#↑s) 2 ^ ℵ₀
rw [generateMeasurable_eq_rec]
α : Type u
s : Set (Set α)
⊢ ((#(Quotient.out (ord (aleph 1))).α) * ⨆ (i : (Quotient.out (ord (aleph 1))).α), #↑(generateMeasurableRec s i)) ≤
    max (#↑s) 2 ^ ℵ₀
α : Type u
s : Set (Set α)
⊢ (#↑(⋃ (i : (Quotient.out (ord (aleph 1))).α), generateMeasurableRec s i)) ≤ max (#↑s) 2 ^ ℵ₀
apply (mk_iUnion_le _).trans
α : Type u
s : Set (Set α)
⊢ (aleph 1 * ⨆ (i : (Quotient.out (ord (aleph 1))).α), #↑(generateMeasurableRec s i)) ≤ max (#↑s) 2 ^ ℵ₀
α : Type u
s : Set (Set α)
⊢ ((#(Quotient.out (ord (aleph 1))).α) * ⨆ (i : (Quotient.out (ord (aleph 1))).α), #↑(generateMeasurableRec s i)) ≤
    max (#↑s) 2 ^ ℵ₀
rw [(aleph 1).mk_ord_out]
α : Type u
s : Set (Set α)
⊢ 𝔠 * max (#↑s) 2 ^ ℵ₀ ≤ max (#↑s) 2 ^ ℵ₀
α : Type u
s : Set (Set α)
⊢ (aleph 1 * ⨆ (i : (Quotient.out (ord (aleph 1))).α), #↑(generateMeasurableRec s i)) ≤ max (#↑s) 2 ^ ℵ₀
refine le_trans (mul_le_mul' aleph_one_le_continuum
    (ciSup_le' fun i => cardinal_generateMeasurableRec_le s i)) ?_
α : Type u
s : Set (Set α)
⊢ 𝔠 ≤ max (#↑s) 2 ^ ℵ₀
α : Type u
s : Set (Set α)
⊢ 𝔠 * max (#↑s) 2 ^ ℵ₀ ≤ max (#↑s) 2 ^ ℵ₀
refine (mul_le_max_of_aleph0_le_left aleph0_le_continuum).trans (max_le ?_ le_rfl)
no goals
α : Type u
s : Set (Set α)
⊢ 𝔠 ≤ max (#↑s) 2 ^ ℵ₀
exact power_le_power_right (le_max_right _ _)