Demostrar con Lean4 que
\n\[ f\u207b\u00b9\left[\bigcap_{i \in I} B_i\right] = \bigcap_{i \in I} f\u207b\u00b9[B_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 (B : I \u2192 Set \u03b2)\n\nexample : f \u207b\u00b9' (\u22c2 i, B i) = \u22c2 i, f \u207b\u00b9' (B i) :=\nby sorry\n<\/pre>\n<\/p>\n
1. Demostraci\u00f3n en lenguaje natural<\/h2>\n
Se demuestra mediante la siguiente cadena de equivalencias
\n\begin{align}
\n x \u2208 f\u207b\u00b9\left[\bigcap_{i \in I} B_i\right]
\n &\u2194 f(x) \u2208 \bigcap_{i \in I} B_i \\
\n &\u2194 (\u2200 i) f(x) \u2208 B_i \\
\n &\u2194 (\u2200 i) x \u2208 f\u207b\u00b9[B_i] \\
\n &\u2194 x \u2208 \bigcap_{i \in I} f\u207b\u00b9[B_i]
\n\end{align}<\/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' (\u22c2 i, B i) = \u22c2 i, f \u207b\u00b9' (B i) :=\nby\n ext x\n -- x : \u03b1\n -- \u22a2 x \u2208 f \u207b\u00b9' \u22c2 (i : I), B i \u2194 x \u2208 \u22c2 (i : I), f \u207b\u00b9' B i\n calc (x \u2208 f \u207b\u00b9' \u22c2 i, B i)\n \u2194 f x \u2208 \u22c2 i, B i := mem_preimage\n _ \u2194 (\u2200 i, f x \u2208 B i) := mem_iInter\n _ \u2194 (\u2200 i, x \u2208 f \u207b\u00b9' B i) := iff_of_eq rfl\n _ \u2194 x \u2208 \u22c2 i, f \u207b\u00b9' B i := mem_iInter.symm\n\n-- 2\u00aa demostraci\u00f3n\n-- ===============\n\nexample : f \u207b\u00b9' (\u22c2 i, B i) = \u22c2 i, f \u207b\u00b9' (B i) :=\nby\n ext x\n -- x : \u03b1\n -- \u22a2 x \u2208 f \u207b\u00b9' \u22c2 (i : I), B i \u2194 x \u2208 \u22c2 (i : I), f \u207b\u00b9' B i\n constructor\n . -- \u22a2 x \u2208 f \u207b\u00b9' \u22c2 (i : I), B i \u2192 x \u2208 \u22c2 (i : I), f \u207b\u00b9' B i\n intro hx\n -- hx : x \u2208 f \u207b\u00b9' \u22c2 (i : I), B i\n -- \u22a2 x \u2208 \u22c2 (i : I), f \u207b\u00b9' B i\n apply mem_iInter_of_mem\n -- \u22a2 \u2200 (i : I), x \u2208 f \u207b\u00b9' B i\n intro i\n -- i : I\n -- \u22a2 x \u2208 f \u207b\u00b9' B i\n rw [mem_preimage]\n -- \u22a2 f x \u2208 B i\n rw [mem_preimage] at hx\n -- hx : f x \u2208 \u22c2 (i : I), B i\n rw [mem_iInter] at hx\n -- hx : \u2200 (i : I), f x \u2208 B i\n exact hx i\n . -- \u22a2 x \u2208 \u22c2 (i : I), f \u207b\u00b9' B i \u2192 x \u2208 f \u207b\u00b9' \u22c2 (i : I), B i\n intro hx\n -- hx : x \u2208 \u22c2 (i : I), f \u207b\u00b9' B i\n -- \u22a2 x \u2208 f \u207b\u00b9' \u22c2 (i : I), B i\n rw [mem_preimage]\n -- \u22a2 f x \u2208 \u22c2 (i : I), B i\n rw [mem_iInter]\n -- \u22a2 \u2200 (i : I), f x \u2208 B i\n intro i\n -- i : I\n -- \u22a2 f x \u2208 B i\n rw [\u2190mem_preimage]\n -- \u22a2 x \u2208 f \u207b\u00b9' B i\n rw [mem_iInter] at hx\n -- hx : \u2200 (i : I), x \u2208 f \u207b\u00b9' B i\n exact hx i\n\n-- 3\u00aa demostraci\u00f3n\n-- ===============\n\nexample : f \u207b\u00b9' (\u22c2 i, B i) = \u22c2 i, f \u207b\u00b9' (B i) :=\nby\n ext x\n -- \u22a2 x \u2208 f \u207b\u00b9' \u22c2 (i : I), B i \u2194 x \u2208 \u22c2 (i : I), f \u207b\u00b9' B i\n simp\n\n-- 4\u00aa demostraci\u00f3n\n-- ===============\n\nexample : f \u207b\u00b9' (\u22c2 i, B i) = \u22c2 i, f \u207b\u00b9' (B i) :=\nby { ext ; simp }\n\n-- Lemas usados\n-- ============\n\n-- variable (x : \u03b1)\n-- variable (s : Set \u03b2)\n-- variable (A : I \u2192 Set \u03b1)\n-- variable (a b : Prop)\n-- #check (iff_of_eq : a = b \u2192 (a \u2194 b))\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_preimage : x \u2208 f \u207b\u00b9' s \u2194 f x \u2208 s)\n<\/pre>\n