Submission Details

Back to Submissions List

Challenge: Cantor's theorem

Submitted by: Violeta Hernández Palacios

Submitted at: 2024-11-19 09:26:48

Code:

import Mathlib

def cantor {α : Type*} (f : α → (α → Bool)) : α → Bool

:= fun x ↦ !f x x

First Theorem Proof:

theorem cantor_not_mem_range {α : Type*} (f : α → (α → Bool)) : cantor f ∉ Set.range f

:= by
  rintro ⟨a, ha⟩ 
  simpa [cantor] using congr_fun ha a

Status: Correct

Feedback: