Demostrar con Lean4 que la composici\u00f3n de funciones suprayectivas es suprayectiva.<\/p>\n
Para ello, completar la siguiente teor\u00eda de Lean4:<\/p>\n
\nimport Mathlib.Tactic\nopen Function\nvariable {\u03b1 : Type _} {\u03b2 : Type _} {\u03b3 : Type _}\nvariable {f : \u03b1 \u2192 \u03b2} {g : \u03b2 \u2192 \u03b3}\n\nexample\n (hg : Surjective g)\n (hf : Surjective f)\n : Surjective (g \u2218 f) :=\nby sorry\n<\/pre>\n<\/p>\n
Demostraci\u00f3n en lenguaje natural<\/b><\/p>\n
\nSupongamos que \(f : A \u2192 B\) y \(g : B \u2192 C\) son suprayectivas. Tenemosque demostrar que
\n\[ (\u2200z \u2208 C)(\u2203x \u2208 A)[g(f(x)) = z] \]
\nSea \(z \u2208 C\). Por ser \(g\) suprayectiva, existe un \(y \u2208 B\) tal que
\n\[ g(y) = z \tag{1} \]
\nPor ser \(f\) suprayectiva, existe un \(x \u2208 A\) tal que
\n\[ f(x) = y \tag{2} \]
\nPor tanto,
\n\begin{align}
\n g(f(x)) &= g(y) &&\text{[por (2)]} \\
\n &= z &&\text{[por (1)]}
\n\end{align}<\/p>\n
Demostraciones con Lean4<\/b><\/p>\n\nimport Mathlib.Tactic\nopen Function\nvariable {\u03b1 : Type _} {\u03b2 : Type _} {\u03b3 : Type _}\nvariable {f : \u03b1 \u2192 \u03b2} {g : \u03b2 \u2192 \u03b3}\n\n-- 1\u00aa demostraci\u00f3n\nexample\n (hg : Surjective g)\n (hf : Surjective f)\n : Surjective (g \u2218 f) :=\nby\n intro z\n -- z : \u03b3\n -- \u22a2 \u2203 a, (g \u2218 f) a = z\n cases' hg z with y hy\n -- y : \u03b2\n -- hy : g y = z\n cases' hf y with x hx\n -- x : \u03b1\n -- hx : f x = y\n use x\n -- \u22a2 (g \u2218 f) x = z\n dsimp\n -- \u22a2 g (f x) = z\n rw [hx]\n -- \u22a2 g y = z\n exact hy\n\n-- 2\u00aa demostraci\u00f3n\nexample\n (hg : Surjective g)\n (hf : Surjective f)\n : Surjective (g \u2218 f) :=\nby\n intro z\n -- z : \u03b3\n -- \u22a2 \u2203 a, (g \u2218 f) a = z\n cases' hg z with y hy\n -- y : \u03b2\n -- hy : g y = z\n cases' hf y with x hx\n -- x : \u03b1\n -- hx : f x = y\n use x\n -- \u22a2 (g \u2218 f) x = z\n dsimp\n -- \u22a2 g (f x) = z\n rw [hx, hy]\n\n-- 3\u00aa demostraci\u00f3n\nexample\n (hg : Surjective g)\n (hf : Surjective f)\n : Surjective (g \u2218 f) :=\nby\n intro z\n -- z : \u03b3\n -- \u22a2 \u2203 a, (g \u2218 f) a = z\n cases' hg z with y hy\n -- y : \u03b2\n -- hy : g y = z\n cases' hf y with x hx\n -- x : \u03b1\n -- hx : f x = y\n exact \u27e8x, by dsimp ; rw [hx, hy]\u27e9\n\n-- 4\u00aa demostraci\u00f3n\nexample\n (hg : Surjective g)\n (hf : Surjective f)\n : Surjective (g \u2218 f) :=\nby\n intro z\n -- z : \u03b3\n -- \u22a2 \u2203 a, (g \u2218 f) a = z\n rcases hg z with \u27e8y, hy : g y = z\u27e9\n rcases hf y with \u27e8x, hx : f x = y\u27e9\n exact \u27e8x, by dsimp ; rw [hx, hy]\u27e9\n\n-- 5\u00aa demostraci\u00f3n\nexample\n (hg : Surjective g)\n (hf : Surjective f)\n : Surjective (g \u2218 f) :=\nSurjective.comp hg hf\n\n-- Lemas usados\n-- ============\n\n-- #check (Surjective.comp : Surjective g \u2192 Surjective f \u2192 Surjective (g \u2218 f))\n<\/pre>\nDemostraciones interactivas<\/b><\/p>\n
Se puede interactuar con las demostraciones anteriores en Lean 4 Web<\/a>.<\/p>\nReferencias<\/b><\/p>\n