Demostrar con Lean4 que
\n\[f[s] \setminus f[t] \u2286 f[s \setminus 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 : f '' s \\ f '' t \u2286 f '' (s \\ t) :=\nby sorry\n<\/pre>\n<\/p>\n
1. Demostraci\u00f3n en lenguaje natural<\/h2>\n
Sea \(y \u2208 f[s] \setminus f[t]\). Entonces,
\n\begin{align}
\n &y \u2208 f[s] \tag{1} \\
\n &y \u2209 f[t] \tag{2}
\n\end{align}
\nPor (1), existe un \(x\) tal que
\n\begin{align}
\n &x \u2208 s \tag{3} \\
\n &f(x) = y \tag{4}
\n\end{align}
\nPor tanto, para demostrar que \(y \u2208 f[s \setminus t]\), basta probar que \(x \u2209 t\). Para ello, supongamos que \(x \u2208 t\). Entonces, por (4), \(y \u2208 f[t]\), en contradicci\u00f3n con (2).<\/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 \\ f '' t \u2286 f '' (s \\ t) :=\nby\n intros y hy\n -- y : \u03b2\n -- hy : y \u2208 f '' s \\ f '' t\n -- \u22a2 y \u2208 f '' (s \\ t)\n rcases hy with \u27e8yfs, ynft\u27e9\n -- yfs : y \u2208 f '' s\n -- ynft : \u00acy \u2208 f '' t\n rcases yfs 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 have h1 : x \u2209 t := by\n intro xt\n -- xt : x \u2208 t\n -- \u22a2 False\n have h2 : f x \u2208 f '' t := mem_image_of_mem f xt\n have h3 : y \u2208 f '' t := by rwa [fxy] at h2\n show False\n exact ynft h3\n have h4 : x \u2208 s \\ t := mem_diff_of_mem xs h1\n have h5 : f x \u2208 f '' (s \\ t) := mem_image_of_mem f h4\n show y \u2208 f '' (s \\ t)\n rwa [fxy] at h5\n\n-- 2\u00aa demostraci\u00f3n\n-- ===============\n\nexample : f '' s \\ f '' t \u2286 f '' (s \\ t) :=\nby\n intros y hy\n -- y : \u03b2\n -- hy : y \u2208 f '' s \\ f '' t\n -- \u22a2 y \u2208 f '' (s \\ t)\n rcases hy with \u27e8yfs, ynft\u27e9\n -- yfs : y \u2208 f '' s\n -- ynft : \u00acy \u2208 f '' t\n rcases yfs 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 s \\ t \u2227 f x = y\n constructor\n . -- \u22a2 x \u2208 s \\ t\n constructor\n . -- \u22a2 x \u2208 s\n exact xs\n . -- \u22a2 \u00acx \u2208 t\n intro xt\n -- xt : x \u2208 t\n -- \u22a2 False\n apply ynft\n -- \u22a2 y \u2208 f '' t\n rw [\u2190fxy]\n -- \u22a2 f x \u2208 f '' t\n apply mem_image_of_mem\n -- \u22a2 x \u2208 t\n exact xt\n . -- \u22a2 f x = y\n exact fxy\n\n-- 3\u00aa demostraci\u00f3n\n-- ===============\n\nexample : f '' s \\ f '' t \u2286 f '' (s \\ t) :=\nby\n rintro y \u27e8\u27e8x, xs, fxy\u27e9, ynft\u27e9\n -- y : \u03b2\n -- ynft : \u00acy \u2208 f '' t\n -- x : \u03b1\n -- xs : x \u2208 s\n -- fxy : f x = y\n -- \u22a2 y \u2208 f '' (s \\ t)\n use x\n -- \u22a2 x \u2208 s \\ t \u2227 f x = y\n aesop\n\n-- 4\u00aa demostraci\u00f3n\n-- ===============\n\nexample : f '' s \\ f '' t \u2286 f '' (s \\ t) :=\nfun y \u27e8\u27e8x, xs, fxy\u27e9, ynft\u27e9 \u21a6 \u27e8x, by aesop\u27e9\n\n-- 5\u00aa demostraci\u00f3n\n-- ===============\n\nexample : f '' s \\ f '' t \u2286 f '' (s \\ t) :=\nsubset_image_diff f s t\n\n-- Lemmas usados\n-- =============\n\n-- variable (x : \u03b1)\n-- #check (mem_image_of_mem f : x \u2208 s \u2192 f x \u2208 f '' s)\n-- #check (subset_image_diff f s t : f '' s \\ f '' t \u2286 f '' (s \\ t))\n<\/pre>\n