Demostrar con Lean4 que
\n\[ f[s] \u2229 t = f[s \u2229 f\u207b\u00b9[t]] \]<\/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 (t : Set \u03b2)\n\nexample : (f '' s) \u2229 t = f '' (s \u2229 f \u207b\u00b9' t) :=\nby sorry\n<\/pre>\n<\/p>\n
1. Demostraci\u00f3n en lenguaje natural<\/h2>\n
Tenemos que demostrar que, para toda \(y\),
\n\[ y \u2208 f[s] \u2229 t \u2194 y \u2208 f[s \u2229 f\u207b\u00b9[t]] \]
\nLo haremos probando las dos implicaciones.<\/p>\n
(\u27f9) Supongamos que \(y \u2208 f[s] \u2229 t\). Entonces, se tiene que
\n\begin{align}
\n &y \u2208 f[s] \tag{1} \\
\n &y \u2208 t \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}
\nPor (2) y (4),
\n\[ f(x) \u2208 t \]
\ny, por tanto,
\n\[ x \u2208 f\u207b\u00b9[t] \]
\nque, junto con (3), da
\n\{ x \u2208 s \u2229 f\u207b\u00b9[t] \]
\ny, por tanto,
\n\[ f(x) \u2208 f[s \u2229 f\u207b\u00b9[t]] \]
\nque, junto con (4), da
\n\[ y \u2208 f[s \u2229 f\u207b\u00b9[t]] \]<\/p>\n
(\u27f8) Supongamos que \(y \u2208 f[s \u2229 f\u207b\u00b9[t]]\). Entonces, existe un \(x\) tal que
\n\begin{align}
\n &x \u2208 s \u2229 f\u207b\u00b9[t] \tag{5} \\
\n &f(x) = y \tag{6}
\n\end{align}
\nPor (1), se tiene que
\n\begin{align}
\n &x \u2208 s \tag{7} \\
\n &x \u2208 f\u207b\u00b9[t] \tag{8}
\n\end{align}
\nPor (7) se tiene que
\n\[ f(x) \u2208 f[s] \]
\ny, junto con (6), se tiene que
\n\[ y \u2208 f[s] \tag{9} \]
\nPor (8), se tiene que
\n\[ f(x) \u2208 t \]
\ny, junto con (6), se tiene que
\n\[ y \u2208 t \tag{10} \]
\nPor (9) y (19), se tiene que
\n\[ y \u2208 f[s] \u2229 t \]<\/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 (t : Set \u03b2)\n\n-- 1\u00aa demostraci\u00f3n\n-- ===============\n\nexample : (f '' s) \u2229 t = f '' (s \u2229 f \u207b\u00b9' t) :=\nby\n ext y\n -- y : \u03b2\n -- \u22a2 y \u2208 f '' s \u2229 t \u2194 y \u2208 f '' (s \u2229 f \u207b\u00b9' t)\n have h1 : y \u2208 f '' s \u2229 t \u2192 y \u2208 f '' (s \u2229 f \u207b\u00b9' t) := by\n intro hy\n -- hy : y \u2208 f '' s \u2229 t\n -- \u22a2 y \u2208 f '' (s \u2229 f \u207b\u00b9' t)\n have h1a : y \u2208 f '' s := hy.1\n obtain \u27e8x : \u03b1, hx: x \u2208 s \u2227 f x = y\u27e9 := h1a\n have h1b : x \u2208 s := hx.1\n have h1c : f x = y := hx.2\n have h1d : y \u2208 t := hy.2\n have h1e : f x \u2208 t := by rwa [\u2190h1c] at h1d\n have h1f : x \u2208 s \u2229 f \u207b\u00b9' t := mem_inter h1b h1e\n have h1g : f x \u2208 f '' (s \u2229 f \u207b\u00b9' t) := mem_image_of_mem f h1f\n show y \u2208 f '' (s \u2229 f \u207b\u00b9' t)\n rwa [h1c] at h1g\n have h2 : y \u2208 f '' (s \u2229 f \u207b\u00b9' t) \u2192 y \u2208 f '' s \u2229 t := by\n intro hy\n -- hy : y \u2208 f '' (s \u2229 f \u207b\u00b9' t)\n -- \u22a2 y \u2208 f '' s \u2229 t\n obtain \u27e8x : \u03b1, hx : x \u2208 s \u2229 f \u207b\u00b9' t \u2227 f x = y\u27e9 := hy\n have h2a : x \u2208 s := hx.1.1\n have h2b : f x \u2208 f '' s := mem_image_of_mem f h2a\n have h2c : y \u2208 f '' s := by rwa [hx.2] at h2b\n have h2d : x \u2208 f \u207b\u00b9' t := hx.1.2\n have h2e : f x \u2208 t := mem_preimage.mp h2d\n have h2f : y \u2208 t := by rwa [hx.2] at h2e\n show y \u2208 f '' s \u2229 t\n exact mem_inter h2c h2f\n show y \u2208 f '' s \u2229 t \u2194 y \u2208 f '' (s \u2229 f \u207b\u00b9' t)\n exact \u27e8h1, h2\u27e9\n\n-- 2\u00aa demostraci\u00f3n\n-- ===============\n\nexample : (f '' s) \u2229 t = f '' (s \u2229 f \u207b\u00b9' t) :=\nby\n ext y\n -- y : \u03b2\n -- \u22a2 y \u2208 f '' s \u2229 t \u2194 y \u2208 f '' (s \u2229 f \u207b\u00b9' t)\n constructor\n . -- \u22a2 y \u2208 f '' s \u2229 t \u2192 y \u2208 f '' (s \u2229 f \u207b\u00b9' t)\n intro hy\n -- hy : y \u2208 f '' s \u2229 t\n -- \u22a2 y \u2208 f '' (s \u2229 f \u207b\u00b9' t)\n cases' hy with hyfs yt\n -- hyfs : y \u2208 f '' s\n -- yt : y \u2208 t\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' t \u2227 f x = y\n constructor\n . -- \u22a2 x \u2208 s \u2229 f \u207b\u00b9' t\n constructor\n . -- \u22a2 x \u2208 s\n exact xs\n . -- \u22a2 x \u2208 f \u207b\u00b9' t\n rw [mem_preimage]\n -- \u22a2 f x \u2208 t\n rw [fxy]\n -- \u22a2 y \u2208 t\n exact yt\n . -- \u22a2 f x = y\n exact fxy\n . -- \u22a2 y \u2208 f '' (s \u2229 f \u207b\u00b9' t) \u2192 y \u2208 f '' s \u2229 t\n intro hy\n -- hy : y \u2208 f '' (s \u2229 f \u207b\u00b9' t)\n -- \u22a2 y \u2208 f '' s \u2229 t\n cases' hy with x hx\n -- x : \u03b1\n -- hx : x \u2208 s \u2229 f \u207b\u00b9' t \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 t\n cases' hx with hx1 fxy\n -- hx1 : x \u2208 s \u2229 f \u207b\u00b9' t\n -- fxy : f x = y\n rw [\u2190fxy]\n -- \u22a2 f x \u2208 t\n rw [\u2190mem_preimage]\n -- \u22a2 x \u2208 f \u207b\u00b9' t\n exact hx1.2\n\n-- 3\u00aa demostraci\u00f3n\n-- ===============\n\nexample : (f '' s) \u2229 t = f '' (s \u2229 f \u207b\u00b9' t) :=\nby\n ext y\n -- y : \u03b2\n -- \u22a2 y \u2208 f '' s \u2229 t \u2194 y \u2208 f '' (s \u2229 f \u207b\u00b9' t)\n constructor\n . -- \u22a2 y \u2208 f '' s \u2229 t \u2192 y \u2208 f '' (s \u2229 f \u207b\u00b9' t)\n rintro \u27e8\u27e8x, xs, fxy\u27e9, yt\u27e9\n -- yt : y \u2208 t\n -- x : \u03b1\n -- xs : x \u2208 s\n -- fxy : f x = y\n -- \u22a2 y \u2208 f '' (s \u2229 f \u207b\u00b9' t)\n use x\n -- \u22a2 x \u2208 s \u2229 f \u207b\u00b9' t \u2227 f x = y\n constructor\n . -- \u22a2 x \u2208 s \u2229 f \u207b\u00b9' t\n constructor\n . -- \u22a2 x \u2208 s\n exact xs\n . -- \u22a2 x \u2208 f \u207b\u00b9' t\n rw [mem_preimage]\n -- \u22a2 f x \u2208 t\n rw [fxy]\n -- \u22a2 y \u2208 t\n exact yt\n . -- \u22a2 f x = y\n exact fxy\n . -- \u22a2 y \u2208 f '' (s \u2229 f \u207b\u00b9' t) \u2192 y \u2208 f '' s \u2229 t\n rintro \u27e8x, \u27e8xs, xt\u27e9, fxy\u27e9\n -- x : \u03b1\n -- fxy : f x = y\n -- xs : x \u2208 s\n -- xt : x \u2208 f \u207b\u00b9' t\n -- \u22a2 y \u2208 f '' s \u2229 t\n constructor\n . -- \u22a2 y \u2208 f '' s\n use x, xs\n -- \u22a2 f x = y\n exact fxy\n . -- \u22a2 y \u2208 t\n rw [\u2190fxy]\n -- \u22a2 f x \u2208 t\n rw [\u2190mem_preimage]\n -- \u22a2 x \u2208 f \u207b\u00b9' t\n exact xt\n\n-- 4\u00aa demostraci\u00f3n\n-- ===============\n\nexample : (f '' s) \u2229 t = f '' (s \u2229 f \u207b\u00b9' t) :=\nby\n ext y\n -- y : \u03b2\n -- \u22a2 y \u2208 f '' s \u2229 t \u2194 y \u2208 f '' (s \u2229 f \u207b\u00b9' t)\n constructor\n . -- \u22a2 y \u2208 f '' s \u2229 t \u2192 y \u2208 f '' (s \u2229 f \u207b\u00b9' t)\n rintro \u27e8\u27e8x, xs, fxy\u27e9, yt\u27e9\n -- yt : y \u2208 t\n -- x : \u03b1\n -- xs : x \u2208 s\n -- fxy : f x = y\n -- \u22a2 y \u2208 f '' (s \u2229 f \u207b\u00b9' t)\n aesop\n . -- \u22a2 y \u2208 f '' (s \u2229 f \u207b\u00b9' t) \u2192 y \u2208 f '' s \u2229 t\n rintro \u27e8x, \u27e8xs, xt\u27e9, fxy\u27e9\n -- x : \u03b1\n -- fxy : f x = y\n -- xs : x \u2208 s\n -- xt : x \u2208 f \u207b\u00b9' t\n -- \u22a2 y \u2208 f '' s \u2229 t\n aesop\n\n-- 5\u00aa demostraci\u00f3n\n-- ===============\n\nexample : (f '' s) \u2229 t = f '' (s \u2229 f \u207b\u00b9' t) :=\nby ext ; constructor <;> aesop\n\n-- 6\u00aa demostraci\u00f3n\n-- ===============\n\nexample : (f '' s) \u2229 t = f '' (s \u2229 f \u207b\u00b9' t) :=\n(image_inter_preimage f s t).symm\n\n-- Lemas usados\n-- ============\n\n-- variable (x : \u03b1)\n-- variable (v : Set \u03b1)\n-- #check (image_inter_preimage f s t : f '' (s \u2229 f \u207b\u00b9' t) = f '' s \u2229 t)\n-- #check (mem_image_of_mem f : x \u2208 s \u2192 f x \u2208 f '' s)\n-- #check (mem_inter : x \u2208 s \u2192 x \u2208 v \u2192 x \u2208 s \u2229 v)\n-- #check (mem_preimage : x \u2208 f \u207b\u00b9' t \u2194 f x \u2208 t)\n<\/pre>\n