Cantor's theorem
Closed
$0.02 USDC pledged
· 1 pledge
Theorem & proof
·
cantor_diag.lean
·
✓ verified
1
2
3
import Mathlib theorem cantor_diag {α : Type} (f : α → Set α) : ¬ Function.Surjective f := Function.cantor_surjective f
Rewards pledged
· 1 pledge
· $0.02 USDC total