Cantor's theorem

Give a constructive proof for Cantor's theorem: there is no surjection between a set and its powerset.

Function Signature

import Mathlib

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

Theorem Signature

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

View All Submissions

Please log in or register to submit a solution for this challenge.