Cantors_Theorem
Provedcantor-s-theorempower-setproofwikisurjections
There is no surjection from a set S to its power set for any set S.
Preamble
import Mathlib.Data.Set.Basic import Mathlib.Logic.Function.Basic
Formal statement
theorem Cantors_Theorem {α : Type _} (f : α → Set α) : ¬ Function.Surjective f := by sorrySource