Cantors_Diagonal_Argument
Provedproofwikiset-theoryuncountable-sets
Let be a set such that , that is, such that is not a singleton. Let be the set of all mappings from the natural numbers to Then is uncountably infinite.
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem Cantors_Diagonal_Argument {S : Type _} (hS : ∃ (a b : S), a ≠ b) : ¬∃ (f : S → (S → S)), Function.Surjective f := by sorrySource