cantor.lean

/-
A constructive proof of the cantor diagonalization argument: there is
no bijection between a set and its powerset.  Since Lean is based on
type theory, we use a type α rather than a set, and for convenience we
use (α → bool) to represent the powerset, i.e. indicator functions on α.
-/

import data.equiv.basic

open function

lemma power_set_not_surjective_image {α : Type*} (f : α → (α → bool)) : ¬surjective f :=
begin
  set h := λ (x : α), !f x x with hdef, -- define h x = !f x x for all x
  intro surj, -- assume f were surjective, by contradiction
  rcases surj h with ⟨x, hx⟩, -- then there would be an x with f x = h
  have key := congr_fun hx x, -- so then f x x = h x
  rw hdef at key, -- substitute in the definition of h
  dsimp only at key, -- now key : f x x = !f x x
  cases f x x; -- which is absurd by a case analysis on the value of f x x
    simp only [bool.bnot_false, bool.bnot_true] at key;
    assumption,
end

theorem cantor_diagonalization (α : Type*) (f : α ≃ (α → bool)) : false :=
begin
  apply power_set_not_surjective_image f.to_fun, -- reduce to showing f is surjective
  exact f.surjective, -- and it is
end