Demostrar con Lean4 que
\n\[ f[\u22c3\u1d62A\u1d62] = \u22c3\u1d62f[A\u1d62] \]<\/p>\n
Para ello, completar la siguiente teor\u00eda de Lean4:<\/p>\n
\nimport Mathlib.Data.Set.Basic\nimport Mathlib.Tactic\n\nopen Set\n\nvariable {\u03b1 \u03b2 I : Type _}\nvariable (f : \u03b1 \u2192 \u03b2)\nvariable (A : \u2115 \u2192 Set \u03b1)\n\nexample : f '' (\u22c3 i, A i) = \u22c3 i, f '' A i :=\nby sorry\n<\/pre>\n<\/p>\n
1. Demostraci\u00f3n en lenguaje natural<\/h2>\n
Tenemos que demostrar que, para todo \(y\),
\n\[ y \u2208 f[\u22c3\u1d62A\u1d62] \u2194 y \u2208 \u22c3\u1d62f[A\u1d62] \]
\nLo haremos demostrando las dos implicaciones.<\/p>\n
(\u27f9) Supongamos que \(y \u2208 f[\u22c3\u1d62A\u1d62]\). Entonces, existe un \(x\) tal que
\n\begin{align}
\n &x \u2208 \u22c3\u1d62A\u1d62 \tag{1} \\
\n &f(x) = y \tag{2}
\n\end{align}
\nPor (1), existe un i tal que
\n\begin{align}
\n &i \u2208 \u2115 \tag{3} \\
\n &x \u2208 A\u1d62 \tag{4}
\n\end{align}
\nPor (4),
\n\[ f(x) \u2208 f[A\u1d62] \]
\nPor (3),
\n\[ f(x) \u2208 \u22c3\u1d62f[A\u1d62] \]
\ny, por (2),
\n\[ y \u2208 \u22c3\u1d62f[A\u1d62] \]<\/p>\n
(\u27f8) Supongamos que \(y \u2208 \u22c3\u1d62f[A\u1d62]\). Entonces, existe un \(i\) tal que
\n\begin{align}
\n &i \u2208 \u2115 \tag{5} \\
\n &y \u2208 f[A\u1d62] \tag{6}
\n\end{align}
\nPor (6), existe un \(x\) tal que
\n\begin{align}
\n &x \u2208 A\u1d62 \tag{7} \\
\n &f(x) = y \tag{8}
\n\end{align}
\nPor (5) y (7),
\n\[ x \u2208 \u22c3\u1d62A\u1d62 \]
\nLuego,
\n\[ f(x) \u2208 f[\u22c3\u1d62A\u1d62] \]
\ny, por (8),
\n\[ y \u2208 f[\u22c3\u1d62A\u1d62] \]<\/p>\n
2. Demostraciones con Lean4<\/h2>\n\nimport Mathlib.Data.Set.Basic\nimport Mathlib.Tactic\n\nopen Set\n\nvariable {\u03b1 \u03b2 I : Type _}\nvariable (f : \u03b1 \u2192 \u03b2)\nvariable (A : \u2115 \u2192 Set \u03b1)\n\n-- 1\u00aa demostraci\u00f3n\n-- ===============\n\nexample : f '' (\u22c3 i, A i) = \u22c3 i, f '' A i :=\nby\n ext y\n -- y : \u03b2\n -- \u22a2 y \u2208 f '' \u22c3 (i : \u2115), A i \u2194 y \u2208 \u22c3 (i : \u2115), f '' A i\n constructor\n . -- \u22a2 y \u2208 f '' \u22c3 (i : \u2115), A i \u2192 y \u2208 \u22c3 (i : \u2115), f '' A i\n intro hy\n -- hy : y \u2208 f '' \u22c3 (i : \u2115), A i\n -- \u22a2 y \u2208 \u22c3 (i : \u2115), f '' A i\n have h1 : \u2203 x, x \u2208 \u22c3 i, A i \u2227 f x = y := (mem_image f (\u22c3 i, A i) y).mp hy\n obtain \u27e8x, hx : x \u2208 \u22c3 i, A i \u2227 f x = y\u27e9 := h1\n have xUA : x \u2208 \u22c3 i, A i := hx.1\n have fxy : f x = y := hx.2\n have xUA : \u2203 i, x \u2208 A i := mem_iUnion.mp xUA\n obtain \u27e8i, xAi : x \u2208 A i\u27e9 := xUA\n have h2 : f x \u2208 f '' A i := mem_image_of_mem f xAi\n have h3 : f x \u2208 \u22c3 i, f '' A i := mem_iUnion_of_mem i h2\n show y \u2208 \u22c3 i, f '' A i\n rwa [fxy] at h3\n . -- \u22a2 y \u2208 \u22c3 (i : \u2115), f '' A i \u2192 y \u2208 f '' \u22c3 (i : \u2115), A i\n intro hy\n -- hy : y \u2208 \u22c3 (i : \u2115), f '' A i\n -- \u22a2 y \u2208 f '' \u22c3 (i : \u2115), A i\n have h4 : \u2203 i, y \u2208 f '' A i := mem_iUnion.mp hy\n obtain \u27e8i, h5 : y \u2208 f '' A i\u27e9 := h4\n have h6 : \u2203 x, x \u2208 A i \u2227 f x = y := (mem_image f (A i) y).mp h5\n obtain \u27e8x, h7 : x \u2208 A i \u2227 f x = y\u27e9 := h6\n have h8 : x \u2208 A i := h7.1\n have h9 : x \u2208 \u22c3 i, A i := mem_iUnion_of_mem i h8\n have h10 : f x \u2208 f '' (\u22c3 i, A i) := mem_image_of_mem f h9\n show y \u2208 f '' (\u22c3 i, A i)\n rwa [h7.2] at h10\n\n-- 2\u00aa demostraci\u00f3n\n-- ===============\n\nexample : f '' (\u22c3 i, A i) = \u22c3 i, f '' A i :=\nby\n ext y\n -- y : \u03b2\n -- \u22a2 y \u2208 f '' \u22c3 (i : \u2115), A i \u2194 y \u2208 \u22c3 (i : \u2115), f '' A i\n constructor\n . -- \u22a2 y \u2208 f '' \u22c3 (i : \u2115), A i \u2192 y \u2208 \u22c3 (i : \u2115), f '' A i\n intro hy\n -- hy : y \u2208 f '' \u22c3 (i : \u2115), A i\n -- \u22a2 y \u2208 \u22c3 (i : \u2115), f '' A i\n rw [mem_image] at hy\n -- hy : \u2203 x, x \u2208 \u22c3 (i : \u2115), A i \u2227 f x = y\n cases' hy with x hx\n -- x : \u03b1\n -- hx : x \u2208 \u22c3 (i : \u2115), A i \u2227 f x = y\n cases' hx with xUA fxy\n -- xUA : x \u2208 \u22c3 (i : \u2115), A i\n -- fxy : f x = y\n rw [mem_iUnion] at xUA\n -- xUA : \u2203 i, x \u2208 A i\n cases' xUA with i xAi\n -- i : \u2115\n -- xAi : x \u2208 A i\n rw [mem_iUnion]\n -- \u22a2 \u2203 i, y \u2208 f '' A i\n use i\n -- \u22a2 y \u2208 f '' A i\n rw [\u2190fxy]\n -- \u22a2 f x \u2208 f '' A i\n apply mem_image_of_mem\n -- \u22a2 x \u2208 A i\n exact xAi\n . -- \u22a2 y \u2208 \u22c3 (i : \u2115), f '' A i \u2192 y \u2208 f '' \u22c3 (i : \u2115), A i\n intro hy\n -- hy : y \u2208 \u22c3 (i : \u2115), f '' A i\n -- \u22a2 y \u2208 f '' \u22c3 (i : \u2115), A i\n rw [mem_iUnion] at hy\n -- hy : \u2203 i, y \u2208 f '' A i\n cases' hy with i yAi\n -- i : \u2115\n -- yAi : y \u2208 f '' A i\n cases' yAi with x hx\n -- x : \u03b1\n -- hx : x \u2208 A i \u2227 f x = y\n cases' hx with xAi fxy\n -- xAi : x \u2208 A i\n -- fxy : f x = y\n rw [\u2190fxy]\n -- \u22a2 f x \u2208 f '' \u22c3 (i : \u2115), A i\n apply mem_image_of_mem\n -- \u22a2 x \u2208 \u22c3 (i : \u2115), A i\n rw [mem_iUnion]\n -- \u22a2 \u2203 i, x \u2208 A i\n use i\n -- \u22a2 x \u2208 A i\n exact xAi\n\n-- 3\u00aa demostraci\u00f3n\n-- ===============\n\nexample : f '' (\u22c3 i, A i) = \u22c3 i, f '' A i :=\nby\n ext y\n -- y : \u03b2\n -- \u22a2 y \u2208 f '' \u22c3 (i : \u2115), A i \u2194 y \u2208 \u22c3 (i : \u2115), f '' A i\n simp\n -- \u22a2 (\u2203 x, (\u2203 i, x \u2208 A i) \u2227 f x = y) \u2194 \u2203 i x, x \u2208 A i \u2227 f x = y\n constructor\n . -- \u22a2 (\u2203 x, (\u2203 i, x \u2208 A i) \u2227 f x = y) \u2192 \u2203 i x, x \u2208 A i \u2227 f x = y\n rintro \u27e8x, \u27e8i, xAi\u27e9, fxy\u27e9\n -- x : \u03b1\n -- fxy : f x = y\n -- i : \u2115\n -- xAi : x \u2208 A i\n -- \u22a2 \u2203 i x, x \u2208 A i \u2227 f x = y\n use i, x, xAi\n -- \u22a2 f x = y\n exact fxy\n . -- \u22a2 (\u2203 i x, x \u2208 A i \u2227 f x = y) \u2192 \u2203 x, (\u2203 i, x \u2208 A i) \u2227 f x = y\n rintro \u27e8i, x, xAi, fxy\u27e9\n -- i : \u2115\n -- x : \u03b1\n -- xAi : x \u2208 A i\n -- fxy : f x = y\n -- \u22a2 \u2203 x, (\u2203 i, x \u2208 A i) \u2227 f x = y\n exact \u27e8x, \u27e8i, xAi\u27e9, fxy\u27e9\n\n-- 4\u00aa demostraci\u00f3n\n-- ===============\n\nexample : f '' (\u22c3 i, A i) = \u22c3 i, f '' A i :=\nimage_iUnion\n\n-- Lemas usados\n-- ============\n\n-- variable (x : \u03b1)\n-- variable (y : \u03b2)\n-- variable (s : Set \u03b1)\n-- variable (i : \u2115)\n-- #check (image_iUnion : f '' \u22c3 i, A i = \u22c3 i, f '' A i)\n-- #check (mem_iUnion : x \u2208 \u22c3 i, A i \u2194 \u2203 i, x \u2208 A i)\n-- #check (mem_iUnion_of_mem i : x \u2208 A i \u2192 x \u2208 \u22c3 i, A i)\n-- #check (mem_image f s y : (y \u2208 f '' s \u2194 \u2203 x, x \u2208 s \u2227 f x = y))\n-- #check (mem_image_of_mem f : x \u2208 s \u2192 f x \u2208 f '' s)\n<\/pre>\n