6 mayo 2022 – Calculemus

Teorema de Cantor

PorJosé A. Alonso 6 mayo 20226 mayo 2022

Demostrar el teorema de Cantor; es decir, que no existe ninguna aplicación suprayectiva de un conjunto en su conjunto potencia.

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

import data.set.basic
open function

variables {α : Type}

example : ∀ f : α → set α, ¬ surjective f :=
sorry

import data.set.basic

open function

variables {α : Type}

example : ∀ f : α → set α, ¬ surjective f :=

sorry