Demostrar que si \(s\) es un subconjunto del dominio de la funci\u00f3n \(f\), entonces \(s\) est\u00e1 contenido en la imagen inversa de la imagen de \(s\) por \(f\); es decir,
\n\[ s \u2286 f\u207b\u00b9[f[s]] \]<\/p>\n
Para ello, completar la siguiente teor\u00eda de Lean4:<\/p>\n
\nimport Mathlib.Data.Set.Function\nopen Set\nvariable {\u03b1 \u03b2 : Type _}\nvariable (f : \u03b1 \u2192 \u03b2)\nvariable (s : Set \u03b1)\n\nexample : s \u2286 f \u207b\u00b9' (f '' s) :=\nby sorry\n<\/pre>\n<\/p>\n
1. Demostraci\u00f3n en lenguaje natural<\/h2>\n
Se demuestra mediante la siguiente cadena de implicaciones
\n\begin{align}
\n x \u2208 s &\u27f9 f(x) \u2208 f[s] \\
\n &\u27f9 x \u2208 f\u207b\u00b9[f[s]]
\n\end{align}<\/p>\n
2. Demostraciones con Lean4<\/h2>\n\nimport Mathlib.Data.Set.Function\n\nopen Set\n\nvariable {\u03b1 \u03b2 : Type _}\nvariable (f : \u03b1 \u2192 \u03b2)\nvariable (s : Set \u03b1)\n\n-- 1\u00aa demostraci\u00f3n\n-- ===============\n\nexample : s \u2286 f \u207b\u00b9' (f '' s) :=\nby\n intros x xs\n -- x : \u03b1\n -- xs : x \u2208 s\n -- \u22a2 x \u2208 f \u207b\u00b9' (f '' s)\n have h1 : f x \u2208 f '' s := mem_image_of_mem f xs\n show x \u2208 f \u207b\u00b9' (f '' s)\n exact mem_preimage.mp h1\n\n-- 2\u00aa demostraci\u00f3n\n-- ===============\n\nexample : s \u2286 f \u207b\u00b9' (f '' s) :=\nby\n intros x xs\n -- x : \u03b1\n -- xs : x \u2208 s\n -- \u22a2 x \u2208 f \u207b\u00b9' (f '' s)\n apply mem_preimage.mpr\n -- \u22a2 f x \u2208 f '' s\n apply mem_image_of_mem\n -- \u22a2 x \u2208 s\n exact xs\n\n-- 3\u00aa demostraci\u00f3n\n-- ===============\n\nexample : s \u2286 f \u207b\u00b9' (f '' s) :=\nby\n intros x xs\n -- x : \u03b1\n -- xs : x \u2208 s\n -- \u22a2 x \u2208 f \u207b\u00b9' (f '' s)\n apply mem_image_of_mem\n -- \u22a2 x \u2208 s\n exact xs\n\n-- 4\u00aa demostraci\u00f3n\n-- ===============\n\nexample : s \u2286 f \u207b\u00b9' (f '' s) :=\nfun _ \u21a6 mem_image_of_mem f\n\n-- 5\u00aa demostraci\u00f3n\n-- ===============\n\nexample : s \u2286 f \u207b\u00b9' (f '' s) :=\nby\n intros x xs\n -- x : \u03b1\n -- xs : x \u2208 s\n -- \u22a2 x \u2208 f \u207b\u00b9' (f '' s)\n show f x \u2208 f '' s\n use x, xs\n\n-- 6\u00aa demostraci\u00f3n\n-- ===============\n\nexample : s \u2286 f \u207b\u00b9' (f '' s) :=\nby\n intros x xs\n -- x : \u03b1\n -- xs : x \u2208 s\n -- \u22a2 x \u2208 f \u207b\u00b9' (f '' s)\n use x, xs\n\n-- 7\u00aa demostraci\u00f3n\n-- ===============\n\nexample : s \u2286 f \u207b\u00b9' (f '' s) :=\nsubset_preimage_image f s\n\n-- Lemas usados\n-- ============\n\n-- variable (x : \u03b1)\n-- variable (t : Set \u03b2)\n-- #check (mem_preimage : x \u2208 f \u207b\u00b9' t \u2194 f x \u2208 t)\n-- #check (mem_image_of_mem f : x \u2208 s \u2192 f x \u2208 f '' s)\n-- #check (subset_preimage_image f s : s \u2286 f \u207b\u00b9' (f '' s))\n<\/pre>\n