Demostrar con Lean4 que
\n\[ f[f\u207b\u00b9[u]] \u2286 u \]<\/p>\n
Para ello, completar la siguiente teor\u00eda de Lean4:<\/p>\n
\nimport Mathlib.Data.Set.Function\nopen Set\n\nvariable {\u03b1 \u03b2 : Type _}\nvariable (f : \u03b1 \u2192 \u03b2)\nvariable (u : Set \u03b2)\n\nexample : f '' (f\u207b\u00b9' u) \u2286 u :=\nby sorry\n<\/pre>\n<\/p>\n
1. Demostraci\u00f3n en lenguaje natural<\/h2>\n
Sea \(y \u2208 f[f\u207b\u00b9[u]]\). Entonces existe un \(x\) tal que
\n\begin{align}
\n &x \u2208 f\u207b\u00b9[u] \tag{1} \\
\n &f(x) = y \tag{2}
\n\end{align}
\nPor (1),
\n\[ f(x) \u2208 u \]
\ny, por (2),
\n\[ y \u2208 u \]<\/p>\n
2. Demostraciones con Lean4<\/h2>\n\nimport Mathlib.Data.Set.Function\nopen Set\n\nvariable {\u03b1 \u03b2 : Type _}\nvariable (f : \u03b1 \u2192 \u03b2)\nvariable (u : Set \u03b2)\n\n-- 1\u00aa demostraci\u00f3n\n-- ===============\n\nexample : f '' (f\u207b\u00b9' u) \u2286 u :=\nby\n intros y h\n -- y : \u03b2\n -- h : y \u2208 f '' (f \u207b\u00b9' u)\n -- \u22a2 y \u2208 u\n obtain \u27e8x : \u03b1, h1 : x \u2208 f \u207b\u00b9' u \u2227 f x = y\u27e9 := h\n obtain \u27e8hx : x \u2208 f \u207b\u00b9' u, fxy : f x = y\u27e9 := h1\n have h2 : f x \u2208 u := mem_preimage.mp hx\n show y \u2208 u\n exact fxy \u25b8 h2\n\n-- 2\u00aa demostraci\u00f3n\n-- ===============\n\nexample : f '' (f\u207b\u00b9' u) \u2286 u :=\nby\n intros y h\n -- y : \u03b2\n -- h : y \u2208 f '' (f \u207b\u00b9' u)\n -- \u22a2 y \u2208 u\n rcases h with \u27e8x, h2\u27e9\n -- x : \u03b1\n -- h2 : x \u2208 f \u207b\u00b9' u \u2227 f x = y\n rcases h2 with \u27e8hx, fxy\u27e9\n -- hx : x \u2208 f \u207b\u00b9' u\n -- fxy : f x = y\n rw [\u2190fxy]\n -- \u22a2 f x \u2208 u\n exact hx\n\n-- 3\u00aa demostraci\u00f3n\n-- ===============\n\nexample : f '' (f\u207b\u00b9' u) \u2286 u :=\nby\n intros y h\n -- y : \u03b2\n -- h : y \u2208 f '' (f \u207b\u00b9' u)\n -- \u22a2 y \u2208 u\n rcases h with \u27e8x, hx, fxy\u27e9\n -- x : \u03b1\n -- hx : x \u2208 f \u207b\u00b9' u\n -- fxy : f x = y\n rw [\u2190fxy]\n -- \u22a2 f x \u2208 u\n exact hx\n\n-- 4\u00aa demostraci\u00f3n\n-- ===============\n\nexample : f '' (f\u207b\u00b9' u) \u2286 u :=\nby\n rintro y \u27e8x, hx, fxy\u27e9\n -- y : \u03b2\n -- x : \u03b1\n -- hx : x \u2208 f \u207b\u00b9' u\n -- fxy : f x = y\n -- \u22a2 y \u2208 u\n rw [\u2190fxy]\n -- \u22a2 f x \u2208 u\n exact hx\n\n-- 5\u00aa demostraci\u00f3n\n-- ===============\n\nexample : f '' (f\u207b\u00b9' u) \u2286 u :=\nby\n rintro y \u27e8x, hx, rfl\u27e9\n -- x : \u03b1\n -- hx : x \u2208 f \u207b\u00b9' u\n -- \u22a2 f x \u2208 u\n exact hx\n\n-- 6\u00aa demostraci\u00f3n\n-- ===============\n\nexample : f '' (f\u207b\u00b9' u) \u2286 u :=\nimage_preimage_subset f u\n\n-- Lemas usados\n-- ============\n\n-- #check (image_preimage_subset f u : f '' (f\u207b\u00b9' u) \u2286 u)\n<\/pre>\n