Cantor's Theorem
Open
Theorem
1
2
-- The power set of any set has strictly greater cardinality than the set itself. theorem cantors_theorem {α : Type*} (f : α → Set α) : ¬Function.Surjective f :=
-- The power set of any set has strictly greater cardinality than the set itself. theorem cantors_theorem {α : Type*} (f : α → Set α) : ¬Function.Surjective f :=