kmill · August 20, 2020 18:01
diff --git a/cantor.lean b/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
	/-
	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