Demostrar con Lean4 que
\n\[ f\left[\bigcap_{i \u2208 I} A_i\right] \u2286 \bigcap_{i \u2208 I} f[A_i] \]<\/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 : I \u2192 Set \u03b1)\n\nexample : f '' (\u22c2 i, A i) \u2286 \u22c2 i, f '' A i :=\nby sorry\n<\/pre>\n<\/p>\n
1. Demostraci\u00f3n en lenguaje natural<\/h2>\n
Sea \(y\) tal que
\n\[ y \u2208 f\left[\bigcap_{i \u2208 I} A\u1d62\right] \tag{1} \]
\nTenemos que demostrar que
\n\[ y \u2208 \bigcap_{i \u2208 I} f[A\u1d62] \]
\nPara ello, sea \(i \u2208 I\), tenemos que demostrar que \(y \u2208 f[A\u1d62]\).<\/p>\n
Por (1), existe un \(x\) tal que
\n\begin{align}
\n &x \u2208 \bigcap_{i \u2208 I} A\u1d62 \tag{2} \\
\n &f(x) = y \tag{3}
\n\end{align}
\nPor (2),
\n\[ x \u2208 A\u1d62 \]
\ny, por tanto,
\n\[ f(x) \u2208 f[A\u1d62] \]
\nque, junto con (3), da que
\n\[ y \u2208 f[A\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 : I \u2192 Set \u03b1)\n\n-- 1\u00aa demostraci\u00f3n\n-- ===============\n\nexample : f '' (\u22c2 i, A i) \u2286 \u22c2 i, f '' A i :=\nby\n intros y h\n -- y : \u03b2\n -- h : y \u2208 f '' \u22c2 (i : I), A i\n -- \u22a2 y \u2208 \u22c2 (i : I), f '' A i\n have h1 : \u2203 x, x \u2208 \u22c2 i, A i \u2227 f x = y := (mem_image f (\u22c2 i, A i) y).mp h\n obtain \u27e8x, hx : x \u2208 \u22c2 i, A i \u2227 f x = y\u27e9 := h1\n have h2 : x \u2208 \u22c2 i, A i := hx.1\n have h3 : f x = y := hx.2\n have h4 : \u2200 i, y \u2208 f '' A i := by\n intro i\n have h4a : x \u2208 A i := mem_iInter.mp h2 i\n have h4b : f x \u2208 f '' A i := mem_image_of_mem f h4a\n show y \u2208 f '' A i\n rwa [h3] at h4b\n show y \u2208 \u22c2 i, f '' A i\n exact mem_iInter.mpr h4\n\n-- 1\u00aa demostraci\u00f3n\n-- ===============\n\nexample : f '' (\u22c2 i, A i) \u2286 \u22c2 i, f '' A i :=\nby\n intros y h\n -- y : \u03b2\n -- h : y \u2208 f '' \u22c2 (i : I), A i\n -- \u22a2 y \u2208 \u22c2 (i : I), f '' A i\n apply mem_iInter_of_mem\n -- \u22a2 \u2200 (i : I), y \u2208 f '' A i\n intro i\n -- i : I\n -- \u22a2 y \u2208 f '' A i\n cases' h with x hx\n -- x : \u03b1\n -- hx : x \u2208 \u22c2 (i : I), A i \u2227 f x = y\n cases' hx with xIA fxy\n -- xIA : x \u2208 \u22c2 (i : I), A i\n -- fxy : f x = y\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 mem_iInter.mp xIA i\n\n-- 2\u00aa demostraci\u00f3n\n-- ===============\n\nexample : f '' (\u22c2 i, A i) \u2286 \u22c2 i, f '' A i :=\nby\n intros y h\n -- y : \u03b2\n -- h : y \u2208 f '' \u22c2 (i : I), A i\n -- \u22a2 y \u2208 \u22c2 (i : I), f '' A i\n apply mem_iInter_of_mem\n -- \u22a2 \u2200 (i : I), y \u2208 f '' A i\n intro i\n -- i : I\n -- \u22a2 y \u2208 f '' A i\n rcases h with \u27e8x, xIA, rfl\u27e9\n -- x : \u03b1\n -- xIA : x \u2208 \u22c2 (i : I), A i\n -- \u22a2 f x \u2208 f '' A i\n exact mem_image_of_mem f (mem_iInter.mp xIA i)\n\n-- 3\u00aa demostraci\u00f3n\n-- ===============\n\nexample : f '' (\u22c2 i, A i) \u2286 \u22c2 i, f '' A i :=\nby\n intro y\n -- y : \u03b2\n -- \u22a2 y \u2208 f '' \u22c2 (i : I), A i \u2192 y \u2208 \u22c2 (i : I), f '' A i\n simp\n -- \u22a2 \u2200 (x : \u03b1), (\u2200 (i : I), x \u2208 A i) \u2192 f x = y \u2192 \u2200 (i : I), \u2203 x, x \u2208 A i \u2227 f x = y\n intros x xIA fxy i\n -- x : \u03b1\n -- xIA : \u2200 (i : I), x \u2208 A i\n -- fxy : f x = y\n -- i : I\n -- \u22a2 \u2203 x, x \u2208 A i \u2227 f x = y\n use x, xIA i\n -- \u22a2 f x = y\n exact fxy\n\n-- 4\u00aa demostraci\u00f3n\n-- ===============\n\nexample : f '' (\u22c2 i, A i) \u2286 \u22c2 i, f '' A i :=\nimage_iInter_subset A f\n\n-- Lemas usados\n-- ============\n\n-- variable (x : \u03b1)\n-- variable (s : Set \u03b1)\n-- #check (image_iInter_subset A f : f '' \u22c2 i, A i \u2286 \u22c2 i, f '' A i)\n-- #check (mem_iInter : x \u2208 \u22c2 i, A i \u2194 \u2200 i, x \u2208 A i)\n-- #check (mem_iInter_of_mem : (\u2200 i, x \u2208 A i) \u2192 x \u2208 \u22c2 i, A i)\n-- #check (mem_image_of_mem f : x \u2208 s \u2192 f x \u2208 f '' s)\n<\/pre>\n