α : Type u
s : Set (Set α)
hs : (#↑s) ≤ 𝔠
⊢ max (#↑s) 2 ^ ℵ₀ ≤ 𝔠 ^ ℵ₀
α : Type u
s : Set (Set α)
hs : (#↑s) ≤ 𝔠
⊢ max (#↑s) 2 ^ ℵ₀ ≤ 𝔠
rw [← continuum_power_aleph0]
no goals
α : Type u
s : Set (Set α)
hs : (#↑s) ≤ 𝔠
⊢ max (#↑s) 2 ^ ℵ₀ ≤ 𝔠 ^ ℵ₀
exact_mod_cast power_le_power_right (max_le hs (nat_lt_continuum 2).le)