Demostrar con Lean4 que si \(s \u2286 t\), entonces \(f[s] \u2286 f[t]\).<\/p>\n
Para ello, completar la siguiente teor\u00eda de Lean4:<\/p>\n
\nimport Mathlib.Data.Set.Function\nimport Mathlib.Tactic\n\nopen Set\n\nvariable {\u03b1 \u03b2 : Type _}\nvariable (f : \u03b1 \u2192 \u03b2)\nvariable (s t : Set \u03b1)\n\nexample\n (h : s \u2286 t)\n : f '' s \u2286 f '' t :=\nby sorry\n<\/pre>\n<\/p>\n
1. Demostraci\u00f3n en lenguaje natural<\/h2>\n
Sea \(y \u2208 f[s]\). Entonces, existe un x tal que
\n\begin{align}
\n &x \u2208 s \tag{1} \\
\n &f(x) = y \tag{2}
\n\end{align}
\nPor (1) y la hip\u00f3tesis,
\n\[ x \u2208 t \tag{3} \]
\nPor (3),
\n\[ f(x) \u2208 f[t] \tag{4} \]
\ny, por (2) y (4),
\n\[ y \u2208 f[t] \]<\/p>\n
2. Demostraciones con Lean4<\/h2>\n\nimport Mathlib.Data.Set.Function\nimport Mathlib.Tactic\n\nopen Set\n\nvariable {\u03b1 \u03b2 : Type _}\nvariable (f : \u03b1 \u2192 \u03b2)\nvariable (s t : Set \u03b1)\n\n-- 1\u00aa demostraci\u00f3n\n-- ===============\n\nexample\n (h : s \u2286 t)\n : f '' s \u2286 f '' t :=\nby\n intros y hy\n -- y : \u03b2\n -- hy : y \u2208 f '' s\n -- \u22a2 y \u2208 f '' t\n rw [mem_image] at hy\n -- hy : \u2203 x, x \u2208 s \u2227 f x = y\n rcases hy with \u27e8x, hx\u27e9\n -- x : \u03b1\n -- hx : x \u2208 s \u2227 f x = y\n rcases hx with \u27e8xs, fxy\u27e9\n -- xs : x \u2208 s\n -- fxy : f x = y\n use x\n -- \u22a2 x \u2208 t \u2227 f x = y\n constructor\n . -- \u22a2 x \u2208 t\n exact h xs\n . -- \u22a2 f x = y\n exact fxy\n\n-- 2\u00aa demostraci\u00f3n\n-- ===============\n\nexample\n (h : s \u2286 t)\n : f '' s \u2286 f '' t :=\nby\n intros y hy\n -- y : \u03b2\n -- hy : y \u2208 f '' s\n -- \u22a2 y \u2208 f '' t\n rcases hy with \u27e8x, xs, fxy\u27e9\n -- x : \u03b1\n -- xs : x \u2208 s\n -- fxy : f x = y\n use x\n -- \u22a2 x \u2208 t \u2227 f x = y\n exact \u27e8h xs, fxy\u27e9\n\n-- 3\u00aa demostraci\u00f3n\n-- ===============\n\nexample\n (h : s \u2286 t)\n : f '' s \u2286 f '' t :=\nimage_subset f h\n\n-- Lemas usados\n-- ============\n\n-- variable (y : \u03b2)\n-- #check (mem_image f s y : y \u2208 f '' s \u2194 \u2203 x, x \u2208 s \u2227 f x = y)\n-- #check (image_subset f : s \u2286 t \u2192 f '' s \u2286 f '' t)\n<\/pre>\n