Demostrar con Lean4 que
\n\[ f[s \u2229 t] \u2286 f[s] \u2229 f[t]\u200b \]<\/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 : f '' (s \u2229 t) \u2286 f '' s \u2229 f '' t :=\nby sorry\n<\/pre>\n<\/p>\n
1. Demostraci\u00f3n en lenguaje natural<\/h2>\n
Sea tal que
\n\[ y \u2208 f[s \u2229 t] \]
\nPor tanto, existe un \(x\) tal que
\n\begin{align}
\n x \u2208 s \u2229 t \tag{1} \\
\n f(x) = y \tag{2}
\n\end{align}
\nPor (1), se tiene que
\n\begin{align}
\n x \u2208 s \tag{3} \\
\n x \u2208 t \tag{4}
\n\end{align}
\nPor (2) y (3), se tiene
\n\[ y \u2208 f[s] \tag{5} \]
\nPor (2) y (4), se tiene
\n\[ y \u2208 f[t] \tag{6} \]
\nPor (5) y (6), se tiene
\n\[ y \u2208 f[s] \u2229 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 : f '' (s \u2229 t) \u2286 f '' s \u2229 f '' t :=\nby\n intros y hy\n -- y : \u03b2\n -- hy : y \u2208 f '' (s \u2229 t)\n -- \u22a2 y \u2208 f '' s \u2229 f '' t\n rcases hy with \u27e8x, hx\u27e9\n -- x : \u03b1\n -- hx : x \u2208 s \u2229 t \u2227 f x = y\n rcases hx with \u27e8xst, fxy\u27e9\n -- xst : x \u2208 s \u2229 t\n -- fxy : f x = y\n constructor\n . -- \u22a2 y \u2208 f '' s\n use x\n -- \u22a2 x \u2208 s \u2227 f x = y\n constructor\n . -- \u22a2 x \u2208 s\n exact xst.1\n . -- \u22a2 f x = y\n exact fxy\n . -- \u22a2 y \u2208 f '' t\n use x\n -- \u22a2 x \u2208 t \u2227 f x = y\n constructor\n . -- \u22a2 x \u2208 t\n exact xst.2\n . -- \u22a2 f x = y\n exact fxy\n\n-- 2\u00aa demostraci\u00f3n\n-- ===============\n\nexample : f '' (s \u2229 t) \u2286 f '' s \u2229 f '' t :=\nby\n intros y hy\n -- y : \u03b2\n -- hy : y \u2208 f '' (s \u2229 t)\n -- \u22a2 y \u2208 f '' s \u2229 f '' t\n rcases hy with \u27e8x, \u27e8xs, xt\u27e9, fxy\u27e9\n -- x : \u03b1\n -- fxy : f x = y\n -- xs : x \u2208 s\n -- xt : x \u2208 t\n constructor\n . -- \u22a2 y \u2208 f '' s\n use x\n -- \u22a2 x \u2208 s \u2227 f x = y\n exact \u27e8xs, fxy\u27e9\n . -- \u22a2 y \u2208 f '' t\n use x\n -- \u22a2 x \u2208 t \u2227 f x = y\n exact \u27e8xt, fxy\u27e9\n\n-- 3\u00aa demostraci\u00f3n\n-- ===============\n\nexample : f '' (s \u2229 t) \u2286 f '' s \u2229 f '' t :=\nimage_inter_subset f s t\n\n-- 4\u00aa demostraci\u00f3n\n-- ===============\n\nexample : f '' (s \u2229 t) \u2286 f '' s \u2229 f '' t :=\nby intro ; aesop\n\n-- Lemas usados\n-- ============\n\n-- #check (image_inter_subset f s t : f '' (s \u2229 t) \u2286 f '' s \u2229 f '' t)\n<\/pre>\n