33. Cantor’s diagonal argument
Cantor’s theorem says that a set is always smaller than the set of its subsets. In Lean, a subset of α can be written as a predicate α → Prop, so the theorem says that no f : α → (α → Prop) is onto.
Prove it constructively: exhibit a predicate S that differs from f a for every a.
Running and submitting solutions, the hints and the editorial come with the Academy Pass. The daily problem is open to every account.
1theorem solution (α : Type) (f : α → (α → Prop)) : ∃ S : α → Prop, ∀ a, f a ≠ S := by
givenLoading editor…
Type
\to in the editor, or click:Where you start. Everything above ⊢ may be assumed; the line below it is what you must prove.
α:Type
f:α → (α → Prop)
⊢∃ S : α → Prop, ∀ a, f a ≠ S
ReadyLn 1, Col 1Lean 4
Draft saved in this browser