Demostrar con Lean4 que
\n\[ f\u207b\u00b9\left[\u22c3\u1d62 B\u1d62\right] = \u22c3\u1d62 f\u207b\u00b9[B\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 (B : I \u2192 Set \u03b2)\n\nexample : f \u207b\u00b9' (\u22c3 i, B i) = \u22c3 i, f \u207b\u00b9' (B i) :=\nby sorry\n<\/pre>\n<\/p>\n
1. Demostraci\u00f3n en lenguaje natural<\/h2>\n
Tenemos que demostrar que, para todo \(x\),
\n\[ x \u2208 f\u207b\u00b9\left[\u22c3\u1d62 B\u1d62\right] \u2194 x \u2208 \u22c3\u1d62 f\u207b\u00b9[B\u1d62] \]
\ny lo haremos demostrando las dos implicaciones.<\/p>\n
(\u27f9) Supongamos que \(x \u2208 f\u207b\u00b9\left[\u22c3\u1d62 B\u1d62\right]\). Entonces, por la definici\u00f3n de la imagen inversa,
\n\[ f(x) \u2208 \u22c3\u1d62 B\u1d62 \]
\ny, por la definici\u00f3n de la uni\u00f3n, existe un \(i\) tal que
\n\[ f(x) \u2208 B\u1d62 \]
\ny, por la definici\u00f3n de la imagen inversa,
\n\[ x \u2208 f\u207b\u00b9[B\u1d62] \]
\ny, por la definici\u00f3n de la uni\u00f3n,
\n\[ x \u2208 \u22c3\u1d62 f\u207b\u00b9[B\u1d62] \]<\/p>\n
(\u27f8) Supongamos que \(x \u2208 \u22c3\u1d62 f\u207b\u00b9[B\u1d62]\). Entonces, por la definici\u00f3n de la uni\u00f3n, existe un \(i\) tal que
\n\[ x \u2208 f\u207b\u00b9[B\u1d62] \]
\ny, por la definici\u00f3n de la imagen inversa,
\n\[ f(x) \u2208 B\u1d62 \]
\ny, por la definici\u00f3n de la uni\u00f3n,
\n\[ f(x) \u2208 \u22c3\u1d62 B\u1d62 \]
\ny, por la definici\u00f3n de la imagen inversa,
\n\[ x \u2208 f\u207b\u00b9\left[\u22c3\u1d62 B\u1d62\right] \]<\/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 (B : I \u2192 Set \u03b2)\n\n-- 1\u00aa demostraci\u00f3n\n-- ===============\n\nexample : f \u207b\u00b9' (\u22c3 i, B i) = \u22c3 i, f \u207b\u00b9' (B i) :=\nby\n ext x\n -- x : \u03b1\n -- \u22a2 x \u2208 f \u207b\u00b9' \u22c3 (i : I), B i \u2194 x \u2208 \u22c3 (i : I), f \u207b\u00b9' B i\n constructor\n . -- \u22a2 x \u2208 f \u207b\u00b9' \u22c3 (i : I), B i \u2192 x \u2208 \u22c3 (i : I), f \u207b\u00b9' B i\n intro hx\n -- hx : x \u2208 f \u207b\u00b9' \u22c3 (i : I), B i\n -- \u22a2 x \u2208 \u22c3 (i : I), f \u207b\u00b9' B i\n rw [mem_preimage] at hx\n -- hx : f x \u2208 \u22c3 (i : I), B i\n rw [mem_iUnion] at hx\n -- hx : \u2203 i, f x \u2208 B i\n cases' hx with i fxBi\n -- i : I\n -- fxBi : f x \u2208 B i\n rw [mem_iUnion]\n -- \u22a2 \u2203 i, x \u2208 f \u207b\u00b9' B i\n use i\n -- \u22a2 x \u2208 f \u207b\u00b9' B i\n apply mem_preimage.mpr\n -- \u22a2 f x \u2208 B i\n exact fxBi\n . -- \u22a2 x \u2208 \u22c3 (i : I), f \u207b\u00b9' B i \u2192 x \u2208 f \u207b\u00b9' \u22c3 (i : I), B i\n intro hx\n -- hx : x \u2208 \u22c3 (i : I), f \u207b\u00b9' B i\n -- \u22a2 x \u2208 f \u207b\u00b9' \u22c3 (i : I), B i\n rw [mem_preimage]\n -- \u22a2 f x \u2208 \u22c3 (i : I), B i\n rw [mem_iUnion]\n -- \u22a2 \u2203 i, f x \u2208 B i\n rw [mem_iUnion] at hx\n -- hx : \u2203 i, x \u2208 f \u207b\u00b9' B i\n cases' hx with i xBi\n -- i : I\n -- xBi : x \u2208 f \u207b\u00b9' B i\n use i\n -- \u22a2 f x \u2208 B i\n rw [mem_preimage] at xBi\n -- xBi : f x \u2208 B i\n exact xBi\n\n-- 2\u00aa demostraci\u00f3n\n-- ===============\n\nexample : f \u207b\u00b9' (\u22c3 i, B i) = \u22c3 i, f \u207b\u00b9' (B i) :=\npreimage_iUnion\n\n-- 3\u00aa demostraci\u00f3n\n-- ===============\n\nexample : f \u207b\u00b9' (\u22c3 i, B i) = \u22c3 i, f \u207b\u00b9' (B i) :=\nby simp\n\n-- Lemas usados\n-- ============\n\n-- variable (x : \u03b1)\n-- variable (s : Set \u03b2)\n-- variable (A : I \u2192 Set \u03b1)\n-- #check (mem_iUnion : x \u2208 \u22c3 i, A i \u2194 \u2203 i, x \u2208 A i)\n-- #check (mem_preimage : x \u2208 f \u207b\u00b9' s \u2194 f x \u2208 s)\n-- #check (preimage_iUnion : f \u207b\u00b9' (\u22c3 i, B i) = \u22c3 i, f \u207b\u00b9' (B i))\n<\/pre>\n