Demostrar con Lean4 que
\n\[ f[s] \u2286 u \u2194 s \u2286 f\u207b\u00b9[u] \]<\/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)\nvariable (u : Set \u03b2)\n\nexample : f '' s \u2286 u \u2194 s \u2286 f \u207b\u00b9' u :=\nby sorry\n<\/pre>\n<\/p>\n
1. Demostraci\u00f3n en lenguaje natural<\/h2>\n
Los demostraremos probando las dos implicaciones.<\/p>\n
(\u27f9) Supongamos que
\n\[ f[s] \u2286 u \tag{1} \]
\ny tenemos que demostrar que
\n\[ s \u2286 f\u207b\u00b9[u] \]
\nSe prueba mediante las siguientes implicaciones
\n\begin{align}
\n x \u2208 s &\u27f9 f(x) \u2208 f[s] \\
\n &\u27f9 f(x) \u2208 u &&\text{[por (1)]} \\
\n &\u27f9 x \u2208 f\u207b\u00b9[u]
\n\end{align}<\/p>\n
(\u27f8) Supongamos que
\n\[ s \u2286 f\u207b\u00b9[u] \tag{2} \]
\ny tenemos que demostrar que
\n\[ f[s] \u2286 u \]
\nPara ello, sea \(y \u2208 f[s]\). Entonces, existe un
\n\[ x \u2208 s \tag{3} \]
\ntal que
\n\[ y = f(x) \tag{4} \]
\nEntonces,
\n\begin{align}
\n &x \u2208 f\u207b\u00b9[u] &&\text{[por (2) y (3)]} \\
\n \u27f9 &f(x) \u2208 u \\
\n \u27f9 &y \u2208 u &&\text{[por (4)]}
\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)\nvariable (u : Set \u03b2)\n\n-- 1\u00aa demostraci\u00f3n\n-- ===============\n\nexample : f '' s \u2286 u \u2194 s \u2286 f \u207b\u00b9' u :=\ncalc f '' s \u2286 u\n \u2194 \u2200 y, y \u2208 f '' s \u2192 y \u2208 u :=\n by simp only [subset_def]\n _ \u2194 \u2200 y, (\u2203 x, x \u2208 s \u2227 f x = y) \u2192 y \u2208 u :=\n by simp only [mem_image]\n _ \u2194 \u2200 x, x \u2208 s \u2192 f x \u2208 u := by\n constructor\n . -- (\u2200 y, (\u2203 x, x \u2208 s \u2227 f x = y) \u2192 y \u2208 u) \u2192 (\u2200 x, x \u2208 s \u2192 f x \u2208 u)\n intro h x xs\n -- h : \u2200 (y : \u03b2), (\u2203 x, x \u2208 s \u2227 f x = y) \u2192 y \u2208 u\n -- x : \u03b1\n -- xs : x \u2208 s\n -- \u22a2 f x \u2208 u\n exact h (f x) (by use x, xs)\n . -- (\u2200 x, x \u2208 s \u2192 f x \u2208 u) \u2192 (\u2200 y, (\u2203 x, x \u2208 s \u2227 f x = y) \u2192 y \u2208 u)\n intro h y hy\n -- h : \u2200 (x : \u03b1), x \u2208 s \u2192 f x \u2208 u\n -- y : \u03b2\n -- hy : \u2203 x, x \u2208 s \u2227 f x = y\n -- \u22a2 y \u2208 u\n obtain \u27e8x, hx\u27e9 := hy\n -- x : \u03b1\n -- hx : x \u2208 s \u2227 f x = y\n have h1 : y = f x := hx.2.symm\n have h2 : f x \u2208 u := h x hx.1\n show y \u2208 u\n exact mem_of_eq_of_mem h1 h2\n _ \u2194 \u2200 x, x \u2208 s \u2192 x \u2208 f \u207b\u00b9' u :=\n by simp only [mem_preimage]\n _ \u2194 s \u2286 f \u207b\u00b9' u :=\n by simp only [subset_def]\n\n-- 2\u00aa demostraci\u00f3n\n-- ===============\n\nexample : f '' s \u2286 u \u2194 s \u2286 f \u207b\u00b9' u :=\ncalc f '' s \u2286 u\n \u2194 \u2200 y, y \u2208 f '' s \u2192 y \u2208 u :=\n by simp only [subset_def]\n _ \u2194 \u2200 y, (\u2203 x, x \u2208 s \u2227 f x = y) \u2192 y \u2208 u :=\n by simp only [mem_image]\n _ \u2194 \u2200 x, x \u2208 s \u2192 f x \u2208 u := by\n constructor\n . -- (\u2200 y, (\u2203 x, x \u2208 s \u2227 f x = y) \u2192 y \u2208 u) \u2192 (\u2200 x, x \u2208 s \u2192 f x \u2208 u)\n intro h x xs\n -- h : \u2200 (y : \u03b2), (\u2203 x, x \u2208 s \u2227 f x = y) \u2192 y \u2208 u\n -- x : \u03b1\n -- xs : x \u2208 s\n -- \u22a2 f x \u2208 u\n apply h (f x)\n -- \u22a2 \u2203 x_1, x_1 \u2208 s \u2227 f x_1 = f x\n use x, xs\n . -- (\u2200 x, x \u2208 s \u2192 f x \u2208 u) \u2192 (\u2200 y, (\u2203 x, x \u2208 s \u2227 f x = y) \u2192 y \u2208 u)\n intro h y hy\n -- h : \u2200 (x : \u03b1), x \u2208 s \u2192 f x \u2208 u\n -- y : \u03b2\n -- hy : \u2203 x, x \u2208 s \u2227 f x = y\n -- \u22a2 y \u2208 u\n obtain \u27e8x, hx\u27e9 := hy\n -- x : \u03b1\n -- hx : x \u2208 s \u2227 f x = y\n rw [\u2190hx.2]\n -- \u22a2 f x \u2208 u\n apply h x\n -- \u22a2 x \u2208 s\n exact hx.1\n _ \u2194 \u2200 x, x \u2208 s \u2192 x \u2208 f \u207b\u00b9' u :=\n by simp only [mem_preimage]\n _ \u2194 s \u2286 f \u207b\u00b9' u :=\n by simp only [subset_def]\n\n-- 3\u00aa demostraci\u00f3n\n-- ===============\n\nexample : f '' s \u2286 u \u2194 s \u2286 f \u207b\u00b9' u :=\nby\n constructor\n . -- \u22a2 f '' s \u2286 u \u2192 s \u2286 f \u207b\u00b9' u\n intros h x xs\n -- h : f '' s \u2286 u\n -- x : \u03b1\n -- xs : x \u2208 s\n -- \u22a2 x \u2208 f \u207b\u00b9' u\n apply mem_preimage.mpr\n -- \u22a2 f x \u2208 u\n apply h\n -- \u22a2 f x \u2208 f '' s\n apply mem_image_of_mem\n -- \u22a2 x \u2208 s\n exact xs\n . -- \u22a2 s \u2286 f \u207b\u00b9' u \u2192 f '' s \u2286 u\n intros h y hy\n -- h : s \u2286 f \u207b\u00b9' u\n -- y : \u03b2\n -- hy : y \u2208 f '' s\n -- \u22a2 y \u2208 u\n rcases hy with \u27e8x, xs, fxy\u27e9\n -- x : \u03b1\n -- xs : x \u2208 s\n -- fxy : f x = y\n rw [\u2190fxy]\n -- \u22a2 f x \u2208 u\n exact h xs\n\n-- 4\u00aa demostraci\u00f3n\n-- ===============\n\nexample : f '' s \u2286 u \u2194 s \u2286 f \u207b\u00b9' u :=\nby\n constructor\n . -- \u22a2 f '' s \u2286 u \u2192 s \u2286 f \u207b\u00b9' u\n intros h x xs\n -- h : f '' s \u2286 u\n -- x : \u03b1\n -- xs : x \u2208 s\n -- \u22a2 x \u2208 f \u207b\u00b9' u\n apply h\n -- \u22a2 f x \u2208 f '' s\n apply mem_image_of_mem\n -- \u22a2 x \u2208 s\n exact xs\n . -- \u22a2 s \u2286 f \u207b\u00b9' u \u2192 f '' s \u2286 u\n rintro h y \u27e8x, xs, rfl\u27e9\n -- h : s \u2286 f \u207b\u00b9' u\n -- x : \u03b1\n -- xs : x \u2208 s\n -- \u22a2 f x \u2208 u\n exact h xs\n\n-- 5\u00aa demostraci\u00f3n\n-- ===============\n\nexample : f '' s \u2286 u \u2194 s \u2286 f \u207b\u00b9' u :=\nimage_subset_iff\n\n-- 4\u00aa demostraci\u00f3n\n-- ===============\n\nexample : f '' s \u2286 u \u2194 s \u2286 f \u207b\u00b9' u :=\nby simp\n\n-- Lemas usados\n-- ============\n\n-- variable (x y : \u03b1)\n-- #check (image_subset_iff : f '' s \u2286 u \u2194 s \u2286 f \u207b\u00b9' u)\n-- #check (mem_image_of_mem f : x \u2208 s \u2192 f x \u2208 f '' s)\n-- #check (mem_of_eq_of_mem : x = y \u2192 y \u2208 s \u2192 x \u2208 s)\n-- #check (mem_preimage : x \u2208 f \u207b\u00b9' u \u2194 f x \u2208 u)\n<\/pre>\n