c : Cardinal
h : ℵ₀ ≤ c
⊢ 2 ^ c ≤ c ^ c

c : Cardinal
h : ℵ₀ ≤ c
⊢ (2 ^ c) ^ c ≤ 2 ^ c
c : Cardinal
h : ℵ₀ ≤ c
⊢ c ^ c = 2 ^ c
apply ((power_le_power_right <| (cantor c).le).trans _).antisymm
no goals
c : Cardinal
h : ℵ₀ ≤ c
⊢ 2 ^ c ≤ c ^ c
exact power_le_power_right ((nat_lt_aleph0 2).le.trans h)
no goals
c : Cardinal
h : ℵ₀ ≤ c
⊢ (2 ^ c) ^ c ≤ 2 ^ c
rw [← power_mul, mul_eq_self h]