Demostrar con Lean4 que si \(f\) es inyectiva, entonces
\n\[\u22c2\u1d62f[A\u1d62] \u2286 f\\left[\u22c2\u1d62A\u1d62\\right] \]<\/p>\n
Para ello, completar la siguiente teor\u00eda de Lean4:<\/p>\n
\nimport Mathlib.Data.Set.Basic\nimport Mathlib.Tactic\n\nopen Set Function\n\nvariable {\u03b1 \u03b2 I : Type _}\nvariable (f : \u03b1 \u2192 \u03b2)\nvariable (A : I \u2192 Set \u03b1)\n\nexample\n (i : I)\n (injf : Injective f)\n : (\u22c2 i, f '' A i) \u2286 f '' (\u22c2 i, A i) :=\nby\nsorry\n<\/pre>\n<\/p>\n
1. Demostraci\u00f3n en lenguaje natural<\/h2>\n
Sea \(y \u2208 \u22c2\u1d62f[A\u1d62]\). Entonces,
\n\begin{align}
\n & (\u2200i \u2208 I)y \u2208 f[A\u1d62] \tag{1} \\
\n & y \u2208 f[A\u1d62]
\n\end{align}
\nPor tanto, existe un \(x \u2208 A\u1d62\) tal que
\n\[ f(x) = y \tag{2} \]<\/p>\n
Veamos que \(x \u2208 \u22c2\u1d62A\u1d62\). Para ello, sea \(j \u2208 I\). Por (1),
\n\[ y \u2208 f[A\u2c7c] \]
\nLuego, existe un \(z\) tal que
\n\begin{align}
\n &z \u2208 A\u2c7c \tag{3} \\
\n &f(z) = y
\n\end{align}
\nPot (2),
\n\[ f(x) = f(z) \]
\ny, por ser \(f\) inyectiva,
\n\[ x = z \]
\ny, por (3),
\n\[ x \u2208 A\u2c7c \]<\/p>\n
Puesto que \(x \u2208 \u22c2\u1d62A\u1d62\) se tiene que \(f(x) \u2208 f\\left[\u22c2\u1d62A\u1d62\\right]\) y, por (2), \(y \u2208 f\\left[\u22c2\u1d62A\u1d62\\right]\).<\/p>\n
2. Demostraciones con Lean4<\/h2>\n\nimport Mathlib.Data.Set.Basic\nimport Mathlib.Tactic\n\nopen Set Function\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\n (i : I)\n (injf : Injective f)\n : (\u22c2 i, f '' A i) \u2286 f '' (\u22c2 i, A i) :=\nby\n intros y hy\n -- y : \u03b2\n -- hy : y \u2208 \u22c2 (i : I), f '' A i\n -- \u22a2 y \u2208 f '' \u22c2 (i : I), A i\n have h1 : \u2200 (i : I), y \u2208 f '' A i := mem_iInter.mp hy\n have h2 : y \u2208 f '' A i := h1 i\n obtain \u27e8x : \u03b1, h3 : x \u2208 A i \u2227 f x = y\u27e9 := h2\n have h4 : f x = y := h3.2\n have h5 : \u2200 i : I, x \u2208 A i := by\n intro j\n have h5a : y \u2208 f '' A j := h1 j\n obtain \u27e8z : \u03b1, h5b : z \u2208 A j \u2227 f z = y\u27e9 := h5a\n have h5c : z \u2208 A j := h5b.1\n have h5d : f z = y := h5b.2\n have h5e : f z = f x := by rwa [\u2190h4] at h5d\n have h5f : z = x := injf h5e\n show x \u2208 A j\n rwa [h5f] at h5c\n have h6 : x \u2208 \u22c2 i, A i := mem_iInter.mpr h5\n have h7 : f x \u2208 f '' (\u22c2 i, A i) := mem_image_of_mem f h6\n show y \u2208 f '' (\u22c2 i, A i)\n rwa [h4] at h7\n\n-- 2\u00aa demostraci\u00f3n\n-- ===============\n\nexample\n (i : I)\n (injf : Injective f)\n : (\u22c2 i, f '' A i) \u2286 f '' (\u22c2 i, A i) :=\nby\n intros y hy\n -- y : \u03b2\n -- hy : y \u2208 \u22c2 (i : I), f '' A i\n -- \u22a2 y \u2208 f '' \u22c2 (i : I), A i\n rw [mem_iInter] at hy\n -- hy : \u2200 (i : I), y \u2208 f '' A i\n rcases hy i with \u27e8x, -, fxy\u27e9\n -- x : \u03b1\n -- fxy : f x = y\n use x\n -- \u22a2 x \u2208 \u22c2 (i : I), A i \u2227 f x = y\n constructor\n . -- \u22a2 x \u2208 \u22c2 (i : I), A i\n apply mem_iInter_of_mem\n -- \u22a2 \u2200 (i : I), x \u2208 A i\n intro j\n -- j : I\n -- \u22a2 x \u2208 A j\n rcases hy j with \u27e8z, zAj, fzy\u27e9\n -- z : \u03b1\n -- zAj : z \u2208 A j\n -- fzy : f z = y\n convert zAj\n -- \u22a2 x = z\n apply injf\n -- \u22a2 f x = f z\n rw [fxy]\n -- \u22a2 y = f z\n rw [\u2190fzy]\n . -- \u22a2 f x = y\n exact fxy\n\n-- 3\u00aa demostraci\u00f3n\n-- ===============\n\nexample\n (i : I)\n (injf : Injective f)\n : (\u22c2 i, f '' A i) \u2286 f '' (\u22c2 i, A i) :=\nby\n intro y\n -- y : \u03b2\n -- \u22a2 y \u2208 \u22c2 (i : I), f '' A i \u2192 y \u2208 f '' \u22c2 (i : I), A i\n simp\n -- \u22a2 (\u2200 (i : I), \u2203 x, x \u2208 A i \u2227 f x = y) \u2192 \u2203 x, (\u2200 (i : I), x \u2208 A i) \u2227 f x = y\n intro h\n -- h : \u2200 (i : I), \u2203 x, x \u2208 A i \u2227 f x = y\n -- \u22a2 \u2203 x, (\u2200 (i : I), x \u2208 A i) \u2227 f x = y\n rcases h i with \u27e8x, -, fxy\u27e9\n -- x : \u03b1\n -- fxy : f x = y\n use x\n -- \u22a2 (\u2200 (i : I), x \u2208 A i) \u2227 f x = y\n constructor\n . -- \u22a2 \u2200 (i : I), x \u2208 A i\n intro j\n -- j : I\n -- \u22a2 x \u2208 A j\n rcases h j with \u27e8z, zAi, fzy\u27e9\n -- z : \u03b1\n -- zAi : z \u2208 A j\n -- fzy : f z = y\n have : f x = f z := by rw [fxy, fzy]\n -- this : f x = f z\n have : x = z := injf this\n -- this : x = z\n rw [this]\n -- \u22a2 z \u2208 A j\n exact zAi\n . -- \u22a2 f x = y\n exact fxy\n\n-- Lemas usados\n-- ============\n\n-- variable (x : \u03b1)\n-- variable (s : Set \u03b1)\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