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