Demostrar con Lean4 que
\n\[ f[s \u222a f\u207b\u00b9[v]] \u2286 f[s] \u222a v \]<\/p>\n
Para ello, completar la siguiente teor\u00eda de Lean4:<\/p>\n
\nimport Mathlib.Data.Set.Function\nimport Mathlib.Tactic\n\nopen Set\n\nvariable (\u03b1 \u03b2 : Type _)\nvariable (f : \u03b1 \u2192 \u03b2)\nvariable (s : Set \u03b1)\nvariable (v : Set \u03b2)\n\nexample : f '' (s \u222a f \u207b\u00b9' v) \u2286 f '' s \u222a v :=\nby sorry\n<\/pre>\n<\/p>\n
1. Demostraci\u00f3n en lenguaje natural<\/h2>\n
Sea \(y \u2208 f[s \u222a f\u207b\u00b9[v]]\). Entonces, existe un x tal que
\n\begin{align}
\n &x \u2208 s \u222a f\u207b\u00b9[v] \tag{1} \\
\n &f(x) = y \tag{2}
\n\end{align}
\nDe (1), se tiene que \(x \u2208 s\) \u00f3 \(x \u2208 f\u207b\u00b9[v]\). Vamos a demostrar en ambos casos que
\n\[ y \u2208 f[s] \u222a v \]<\/p>\n
Caso 1<\/strong>: Supongamos que \(x \u2208 s\). Entonces,
\n\[ f(x) \u2208 f[s] \]
\ny, por (2), se tiene que
\n\[ y \u2208 f[s] \]
\nPor tanto,
\n\[ y \u2208 f[s] \u222a v \]<\/p>\nCaso 2<\/strong>: Supongamos que \(x \u2208 f\u207b\u00b9[v]\). Entonces,
\n\[ f(x) \u2208 v \]
\ny, por (2), se tiene que
\n\[ y \u2208 v \]
\nPor tanto,
\n\[ y \u2208 f[s] \u222a v \]<\/p>\n2. Demostraciones con Lean4<\/h2>\n\nimport Mathlib.Data.Set.Function\nimport Mathlib.Tactic\n\nopen Set\n\nvariable (\u03b1 \u03b2 : Type _)\nvariable (f : \u03b1 \u2192 \u03b2)\nvariable (s : Set \u03b1)\nvariable (v : Set \u03b2)\n\n-- 1\u00aa demostraci\u00f3n\n-- ===============\n\nexample : f '' (s \u222a f \u207b\u00b9' v) \u2286 f '' s \u222a v :=\nby\n intros y hy\n obtain \u27e8x : \u03b1, hx : x \u2208 s \u222a f \u207b\u00b9' v \u2227 f x = y\u27e9 := hy\n obtain \u27e8hx1 : x \u2208 s \u222a f \u207b\u00b9' v, fxy : f x = y\u27e9 := hx\n cases' hx1 with xs xv\n . -- xs : x \u2208 s\n have h1 : f x \u2208 f '' s := mem_image_of_mem f xs\n have h2 : y \u2208 f '' s := by rwa [fxy] at h1\n show y \u2208 f '' s \u222a v\n exact mem_union_left v h2\n . -- xv : x \u2208 f \u207b\u00b9' v\n have h3 : f x \u2208 v := mem_preimage.mp xv\n have h4 : y \u2208 v := by rwa [fxy] at h3\n show y \u2208 f '' s \u222a v\n exact mem_union_right (f '' s) h4\n\n-- 1\u00aa demostraci\u00f3n\n-- ===============\n\nexample : f '' (s \u222a f \u207b\u00b9' v) \u2286 f '' s \u222a v :=\nby\n intros y hy\n obtain \u27e8x : \u03b1, hx : x \u2208 s \u222a f \u207b\u00b9' v \u2227 f x = y\u27e9 := hy\n obtain \u27e8hx1 : x \u2208 s \u222a f \u207b\u00b9' v, fxy : f x = y\u27e9 := hx\n cases' hx1 with xs xv\n . -- xs : x \u2208 s\n left\n -- \u22a2 y \u2208 f '' s\n use x\n -- \u22a2 x \u2208 s \u2227 f x = y\n constructor\n . -- \u22a2 x \u2208 s\n exact xs\n . -- \u22a2 f x = y\n exact fxy\n . -- \u22a2 y \u2208 f '' s \u222a v\n right\n -- \u22a2 y \u2208 v\n rw [\u2190fxy]\n -- \u22a2 f x \u2208 v\n exact xv\n\n-- 2\u00aa demostraci\u00f3n\n-- ===============\n\nexample : f '' (s \u222a f \u207b\u00b9' v) \u2286 f '' s \u222a v :=\nby\n rintro y \u27e8x, xs | xv, fxy\u27e9\n -- y : \u03b2\n -- x : \u03b1\n . -- xs : x \u2208 s\n -- \u22a2 y \u2208 f '' s \u222a v\n left\n -- \u22a2 y \u2208 f '' s\n use x, xs\n -- \u22a2 f x = y\n exact fxy\n . -- xv : x \u2208 f \u207b\u00b9' v\n -- \u22a2 y \u2208 f '' s \u222a v\n right\n -- \u22a2 y \u2208 v\n rw [\u2190fxy]\n -- \u22a2 f x \u2208 v\n exact xv\n\n-- 3\u00aa demostraci\u00f3n\n-- ===============\n\nexample : f '' (s \u222a f \u207b\u00b9' v) \u2286 f '' s \u222a v :=\nby\n rintro y \u27e8x, xs | xv, fxy\u27e9 <;>\n aesop\n\n-- Lemas usados\n-- ============\n\n-- variable (x : \u03b1)\n-- variable (t : Set \u03b1)\n-- #check (mem_image_of_mem f : x \u2208 s \u2192 f x \u2208 f '' s)\n-- #check (mem_preimage : x \u2208 f \u207b\u00b9' v \u2194 f x \u2208 v)\n-- #check (mem_union_left t : x \u2208 s \u2192 x \u2208 s \u222a t)\n-- #check (mem_union_right s : x \u2208 t \u2192 x \u2208 s \u222a t)\n<\/pre>\n