2 mayo 2024 – Calculemus

Teorema de Cantor

PorJosé A. Alonso 2 mayo 2024

Demostrar con Lean4 el teorema de Cantor; es decir, que no existe ninguna aplicación suprayectiva de un conjunto en el conjunto de sus subconjuntos.

Para ello, completar la siguiente teoría de Lean4:

import Mathlib.Data.Set.Basic
open Function

variable {α : Type}

example : ∀ f : α → Set α, ¬Surjective f :=
by sorry

import Mathlib.Data.Set.Basic

open Function

variable {α : Type}

example : ∀ f : α → Set α, ¬Surjective f :=

by sorry