Demostrar con Lean4 que
\n\[ f[s] \u2229 v = f[s \u2229 f\u207b\u00b9[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) \u2229 v = f '' (s \u2229 f \u207b\u00b9' v) :=\nby sorry\n<\/pre>\n<\/p>\n
1. Demostraci\u00f3n en lenguaje natural<\/h2>\n
Tenemmos que demostrar que, para todo \(y\),
\n\[ y \u2208 f[s] \u2229 v \u2194 y \u2208 f[s \u2229 f\u207b\u00b9[v]] \]
\nLo haremos demostrando las dos implicaciones.<\/p>\n
(\u27f9) Supongamos que \(y \u2208 f[s] \u2229 v\). Entonces,
\n\begin{align}
\n &y \u2208 f[s] \tag{1} \\
\n &y \u2208 v \tag{2}
\n\end{align}
\nPor (1), existe un \(x\) tal que
\n\begin{align}
\n &x \u2208 s \tag{3} \\
\n &f(x) = y \tag{4}
\n\end{align}
\nDe (2) y (4), se tiene que
\n\[ f(x) \u2208 v \]
\ny, por tanto,
\n\[ x \u2208 f\u207b\u00b9[v] \tag{5} \]
\nDe (3) y (5), se tiene que
\n\[ x \u2208 s \u2229 f\u207b\u00b9[v] \]
\nPor tanto,
\n\[ f(x) \u2208 f[s \u2229 f\u207b\u00b9[v]] \]
\ny, por (4),
\n\[ y \u2208 f[s \u2229 f\u207b\u00b9[v]] \]<\/p>\n
(\u27f8) Supongamos que \(y \u2208 f[s \u2229 f\u207b\u00b9[v]]\). Entonces, existe un \(x\) tal que
\n\begin{align}
\n &x \u2208 s \u2229 f\u207b\u00b9[v] \tag{6} \\
\n &f(x) = y \tag{7}
\n\end{align}
\nPor (6), se tiene que
\n\begin{align}
\n &x \u2208 s \tag{8} \\
\n &x \u2208 f\u207b\u00b9[v] \tag{9}
\n\end{align}
\nPor (8), se tiene que
\n\[ f(x) \u2208 f[s] \]
\ny, por (7),
\n\[ y \u2208 f[s] \tag{10} \]
\nPor (9),
\n\[ f(x) \u2208 v \]
\ny, por (7),
\n\[ y \u2208 v \tag{11} \]
\nPor (10) y (11),
\n\[ y \u2208 f[s] \u2229 v \]<\/p>\n
2. 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) \u2229 v = f '' (s \u2229 f \u207b\u00b9' v) :=\nby\n ext y\n -- y : \u03b2\n -- \u22a2 y \u2208 f '' s \u2229 v \u2194 y \u2208 f '' (s \u2229 f \u207b\u00b9' v)\n constructor\n . -- \u22a2 y \u2208 f '' s \u2229 v \u2192 y \u2208 f '' (s \u2229 f \u207b\u00b9' v)\n intro hy\n -- hy : y \u2208 f '' s \u2229 v\n -- \u22a2 y \u2208 f '' (s \u2229 f \u207b\u00b9' v)\n cases' hy with hyfs yv\n -- hyfs : y \u2208 f '' s\n -- yv : y \u2208 v\n cases' hyfs with x hx\n -- x : \u03b1\n -- hx : x \u2208 s \u2227 f x = y\n cases' hx with xs fxy\n -- xs : x \u2208 s\n -- fxy : f x = y\n have h1 : f x \u2208 v := by rwa [\u2190fxy] at yv\n have h3 : x \u2208 s \u2229 f \u207b\u00b9' v := mem_inter xs h1\n have h4 : f x \u2208 f '' (s \u2229 f \u207b\u00b9' v) := mem_image_of_mem f h3\n show y \u2208 f '' (s \u2229 f \u207b\u00b9' v)\n rwa [fxy] at h4\n . -- \u22a2 y \u2208 f '' (s \u2229 f \u207b\u00b9' v) \u2192 y \u2208 f '' s \u2229 v\n intro hy\n -- hy : y \u2208 f '' (s \u2229 f \u207b\u00b9' v)\n -- \u22a2 y \u2208 f '' s \u2229 v\n cases' hy with x hx\n -- x : \u03b1\n -- hx : x \u2208 s \u2229 f \u207b\u00b9' v \u2227 f x = y\n cases' hx with hx1 fxy\n -- hx1 : x \u2208 s \u2229 f \u207b\u00b9' v\n -- fxy : f x = y\n cases' hx1 with xs xfv\n -- xs : x \u2208 s\n -- xfv : x \u2208 f \u207b\u00b9' v\n have h5 : f x \u2208 f '' s := mem_image_of_mem f xs\n have h6 : y \u2208 f '' s := by rwa [fxy] at h5\n have h7 : f x \u2208 v := mem_preimage.mp xfv\n have h8 : y \u2208 v := by rwa [fxy] at h7\n show y \u2208 f '' s \u2229 v\n exact mem_inter h6 h8\n\n-- 2\u00aa demostraci\u00f3n\n-- ===============\n\nexample : (f '' s) \u2229 v = f '' (s \u2229 f \u207b\u00b9' v) :=\nby\n ext y\n -- y : \u03b2\n -- \u22a2 y \u2208 f '' s \u2229 v \u2194 y \u2208 f '' (s \u2229 f \u207b\u00b9' v)\n constructor\n . -- \u22a2 y \u2208 f '' s \u2229 v \u2192 y \u2208 f '' (s \u2229 f \u207b\u00b9' v)\n intro hy\n -- hy : y \u2208 f '' s \u2229 v\n -- \u22a2 y \u2208 f '' (s \u2229 f \u207b\u00b9' v)\n cases' hy with hyfs yv\n -- hyfs : y \u2208 f '' s\n -- yv : y \u2208 v\n cases' hyfs with x hx\n -- x : \u03b1\n -- hx : x \u2208 s \u2227 f x = y\n cases' hx with xs fxy\n -- xs : x \u2208 s\n -- fxy : f x = y\n use x\n -- \u22a2 x \u2208 s \u2229 f \u207b\u00b9' v \u2227 f x = y\n constructor\n . -- \u22a2 x \u2208 s \u2229 f \u207b\u00b9' v\n constructor\n . -- \u22a2 x \u2208 s\n exact xs\n . -- \u22a2 x \u2208 f \u207b\u00b9' v\n rw [mem_preimage]\n -- \u22a2 f x \u2208 v\n rw [fxy]\n -- \u22a2 y \u2208 v\n exact yv\n . -- \u22a2 f x = y\n exact fxy\n . -- \u22a2 y \u2208 f '' (s \u2229 f \u207b\u00b9' v) \u2192 y \u2208 f '' s \u2229 v\n intro hy\n -- hy : y \u2208 f '' (s \u2229 f \u207b\u00b9' v)\n -- \u22a2 y \u2208 f '' s \u2229 v\n cases' hy with x hx\n -- x : \u03b1\n -- hx : x \u2208 s \u2229 f \u207b\u00b9' v \u2227 f x = y\n constructor\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 hx.1.1\n . -- \u22a2 f x = y\n exact hx.2\n . -- \u22a2 y \u2208 v\n cases' hx with hx1 fxy\n -- hx1 : x \u2208 s \u2229 f \u207b\u00b9' v\n -- fxy : f x = y\n rw [\u2190fxy]\n -- \u22a2 f x \u2208 v\n rw [\u2190mem_preimage]\n -- \u22a2 x \u2208 f \u207b\u00b9' v\n exact hx1.2\n\n-- 3\u00aa demostraci\u00f3n\n-- ===============\n\nexample : (f '' s) \u2229 v = f '' (s \u2229 f \u207b\u00b9' v) :=\nby\n ext y\n -- y : \u03b2\n -- \u22a2 y \u2208 f '' s \u2229 v \u2194 y \u2208 f '' (s \u2229 f \u207b\u00b9' v)\n constructor\n . -- \u22a2 y \u2208 f '' s \u2229 v \u2192 y \u2208 f '' (s \u2229 f \u207b\u00b9' v)\n rintro \u27e8\u27e8x, xs, fxy\u27e9, yv\u27e9\n -- yv : y \u2208 v\n -- x : \u03b1\n -- xs : x \u2208 s\n -- fxy : f x = y\n -- \u22a2 y \u2208 f '' (s \u2229 f \u207b\u00b9' v)\n use x\n -- \u22a2 x \u2208 s \u2229 f \u207b\u00b9' v \u2227 f x = y\n constructor\n . -- \u22a2 x \u2208 s \u2229 f \u207b\u00b9' v\n constructor\n . -- \u22a2 x \u2208 s\n exact xs\n . -- \u22a2 x \u2208 f \u207b\u00b9' v\n rw [mem_preimage]\n -- \u22a2 f x \u2208 v\n rw [fxy]\n -- \u22a2 y \u2208 v\n exact yv\n . exact fxy\n . rintro \u27e8x, \u27e8xs, xv\u27e9, fxy\u27e9\n -- x : \u03b1\n -- fxy : f x = y\n -- xs : x \u2208 s\n -- xv : x \u2208 f \u207b\u00b9' v\n -- \u22a2 y \u2208 f '' s \u2229 v\n constructor\n . -- \u22a2 y \u2208 f '' s\n use x, xs\n -- \u22a2 f x = y\n exact fxy\n . -- \u22a2 y \u2208 v\n rw [\u2190fxy]\n -- \u22a2 f x \u2208 v\n rw [\u2190mem_preimage]\n -- \u22a2 x \u2208 f \u207b\u00b9' v\n exact xv\n\n-- 4\u00aa demostraci\u00f3n\n-- ===============\n\nexample : (f '' s) \u2229 v = f '' (s \u2229 f \u207b\u00b9' v) :=\nby\n ext y\n -- y : \u03b2\n -- \u22a2 y \u2208 f '' s \u2229 v \u2194 y \u2208 f '' (s \u2229 f \u207b\u00b9' v)\n constructor\n . -- \u22a2 y \u2208 f '' s \u2229 v \u2192 y \u2208 f '' (s \u2229 f \u207b\u00b9' v)\n rintro \u27e8\u27e8x, xs, fxy\u27e9, yv\u27e9\n -- yv : y \u2208 v\n -- x : \u03b1\n -- xs : x \u2208 s\n -- fxy : f x = y\n -- \u22a2 y \u2208 f '' (s \u2229 f \u207b\u00b9' v)\n aesop\n . -- \u22a2 y \u2208 f '' (s \u2229 f \u207b\u00b9' v) \u2192 y \u2208 f '' s \u2229 v\n rintro \u27e8x, \u27e8xs, xv\u27e9, fxy\u27e9\n -- x : \u03b1\n -- fxy : f x = y\n -- xs : x \u2208 s\n -- xv : x \u2208 f \u207b\u00b9' v\n -- \u22a2 y \u2208 f '' s \u2229 v\n aesop\n\n-- 5\u00aa demostraci\u00f3n\n-- ===============\n\nexample : (f '' s) \u2229 v = f '' (s \u2229 f \u207b\u00b9' v) :=\nby ext ; constructor <;> aesop\n\n-- 6\u00aa demostraci\u00f3n\n-- ===============\n\nexample : (f '' s) \u2229 v = f '' (s \u2229 f \u207b\u00b9' v) :=\n(image_inter_preimage f s v).symm\n\n-- Lemas usados\n-- ============\n\n-- variable (x : \u03b1)\n-- variable (a b : Set \u03b1)\n-- #check (image_inter_preimage f s v : f '' (s \u2229 f \u207b\u00b9' v) = f '' s \u2229 v)\n-- #check (mem_image_of_mem f : x \u2208 a \u2192 f x \u2208 f '' a)\n-- #check (mem_inter : x \u2208 a \u2192 x \u2208 b \u2192 x \u2208 a \u2229 b)\n-- #check (mem_preimage : x \u2208 f \u207b\u00b9' v \u2194 f x \u2208 v)\n<\/pre>\n