α : Type ?u.58
β : Type ?u.61
γ : Type ?u.64
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
σ : Type u
x✝ : Nonempty (Cardinal ↪ σ)
f : Cardinal → σ
hf : Injective f
g : σ → Cardinal := Function.invFun f
x : σ
hx : g x = 2 ^ sum g
this : g x ≤ sum g
⊢ 2 ^ sum g > sum g
α : Type ?u.58
β : Type ?u.61
γ : Type ?u.64
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
σ : Type u
x✝ : Nonempty (Cardinal ↪ σ)
f : Cardinal → σ
hf : Injective f
g : σ → Cardinal := Function.invFun f
x : σ
hx : g x = 2 ^ sum g
this : g x ≤ sum g
⊢ g x > sum g
rw [hx]
no goals
α : Type ?u.58
β : Type ?u.61
γ : Type ?u.64
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
σ : Type u
x✝ : Nonempty (Cardinal ↪ σ)
f : Cardinal → σ
hf : Injective f
g : σ → Cardinal := Function.invFun f
x : σ
hx : g x = 2 ^ sum g
this : g x ≤ sum g
⊢ 2 ^ sum g > sum g
exact cantor _