Submission Details

Back to Submissions List

Challenge: Cantor's theorem

Submitted by: fogofchess

Submitted at: 2024-11-23 20:37:44

Code:

import Mathlib

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

:= fun a =>
  Bool.not (f a a)

First Theorem Proof:

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

:= by
  unfold cantor
  simp only [Set.mem_range, not_exists]
  intro x h
  have h' := congr_fun h x
  simp at h'

Status: Correct

Feedback: