Demostrar con Lean4 el teorema de Cantor; es decir, que no existe ninguna aplicaci\u00f3n suprayectiva de un conjunto en el conjunto de sus subconjuntos.<\/p>\n
Para ello, completar la siguiente teor\u00eda de Lean4:<\/p>\n
\nimport Mathlib.Data.Set.Basic\nopen Function\n\nvariable {\u03b1 : Type}\n\nexample : \u2200 f : \u03b1 \u2192 Set \u03b1, \u00acSurjective f :=\nby sorry\n<\/pre>\n<\/p>\n
1. Demostraci\u00f3n en lenguaje natural<\/h2>\n
Sea \(f\) una funci\u00f3n de \(A\) en el conjunto de los subconjuntos \(A\). Tenemos que demostrar que \(f\) no es suprayectiva. Lo haremos por reducci\u00f3n al absurdo. Para ello, supongamos que \(f\) es suprayectiva y consideremos el conjunto
\n\[ S := \{i \u2208 A | i \u2209 f(i)\} \tag{1} \]
\nEntonces, tiene que existir un \(j \u2208 A\) tal que
\n\[ f(j) = S \tag{2} \]
\nSe pueden dar dos casos: \(j \u2208 S\) \u00f3 \(j \u2209 S\). Veamos que ambos son imposibles.<\/p>\n
Caso 1: Supongamos que \(j \u2208 S\). Entonces, por (1)
\n\[ j \u2209 f(j) \]
\ny, por (2),
\n\[ j \u2209 S \]
\nque es una contradicci\u00f3n.<\/p>\n
Caso 2: Supongamos que \(j \u2209 S\). Entonces, por (1)
\n\[ j \u2208 f(j) \]
\ny, por (2),
\n\[ j \u2208 S \]
\nque es una contradicci\u00f3n.<\/p>\n
2. Demostraciones con Lean4<\/h2>\n\nimport Mathlib.Data.Set.Basic\nopen Function\n\nvariable {\u03b1 : Type}\n\n-- 1\u00aa demostraci\u00f3n\n-- ===============\n\nexample : \u2200 f : \u03b1 \u2192 Set \u03b1, \u00acSurjective f :=\nby\n intros f hf\n -- f : \u03b1 \u2192 Set \u03b1\n -- hf : Surjective f\n -- \u22a2 False\n let S := {i | i \u2209 f i}\n unfold Surjective at hf\n -- hf : \u2200 (b : Set \u03b1), \u2203 a, f a = b\n cases' hf S with j hj\n -- j : \u03b1\n -- hj : f j = S\n by_cases j \u2208 S\n . -- h : j \u2208 S\n dsimp at h\n -- h : \u00acj \u2208 f j\n apply h\n -- \u22a2 j \u2208 f j\n rw [hj]\n -- \u22a2 j \u2208 S\n exact h\n . -- h : \u00acj \u2208 S\n apply h\n -- \u22a2 j \u2208 S\n rw [\u2190hj] at h\n -- h : \u00acj \u2208 f j\n exact h\n\n-- 2\u00aa demostraci\u00f3n\n-- ===============\n\nexample : \u2200 f : \u03b1 \u2192 Set \u03b1, \u00ac Surjective f :=\nby\n intros f hf\n -- f : \u03b1 \u2192 Set \u03b1\n -- hf : Surjective f\n -- \u22a2 False\n let S := {i | i \u2209 f i}\n cases' hf S with j hj\n -- j : \u03b1\n -- hj : f j = S\n by_cases j \u2208 S\n . -- h : j \u2208 S\n apply h\n -- \u22a2 j \u2208 f j\n rwa [hj]\n . -- h : \u00acj \u2208 S\n apply h\n rwa [\u2190hj] at h\n\n-- 3\u00aa demostraci\u00f3n\n-- ===============\n\nexample : \u2200 f : \u03b1 \u2192 Set \u03b1, \u00ac Surjective f :=\nby\n intros f hf\n -- f : \u03b1 \u2192 Set \u03b1\n -- hf : Surjective f\n -- \u22a2 False\n let S := {i | i \u2209 f i}\n cases' hf S with j hj\n -- j : \u03b1\n -- hj : f j = S\n have h : (j \u2208 S) = (j \u2209 S) :=\n calc (j \u2208 S)\n = (j \u2209 f j) := Set.mem_setOf_eq\n _ = (j \u2209 S) := congrArg (j \u2209 .) hj\n exact iff_not_self (iff_of_eq h)\n\n-- 4\u00aa demostraci\u00f3n\n-- ===============\n\nexample : \u2200 f : \u03b1 \u2192 Set \u03b1, \u00ac Surjective f :=\ncantor_surjective\n\n-- Lemas usados\n-- ============\n\n-- variable (x : \u03b1)\n-- variable (p : \u03b1 \u2192 Prop)\n-- variable (a b : Prop)\n-- #check (Set.mem_setOf_eq : (x \u2208 {y : \u03b1 | p y}) = p x)\n-- #check (iff_of_eq : a = b \u2192 (a \u2194 b))\n-- #check (iff_not_self : \u00ac(a \u2194 \u00aca))\n-- #check (cantor_surjective : \u2200 f : \u03b1 \u2192 Set \u03b1, \u00ac Surjective f)\n<\/pre>\n