Demostrar con Lean4 que si \(f\) es inyectiva, entonces
\n\[ f[s] \u2229 f[t] \u2286 f[s \u2229 t] \]<\/p>\n
Para ello, completar la siguiente teor\u00eda de Lean4:<\/p>\n
\nimport Mathlib.Data.Set.Function\n\nopen Set Function\n\nvariable {\u03b1 \u03b2 : Type _}\nvariable (f : \u03b1 \u2192 \u03b2)\nvariable (s t : Set \u03b1)\n\nexample\n (h : Injective f)\n : f '' s \u2229 f '' t \u2286 f '' (s \u2229 t) :=\nby sorry\n<\/pre>\n<\/p>\n
1. Demostraci\u00f3n en lenguaje natural<\/h2>\n
Sea \(y \u2208 f[s] \u2229 f[t]\). Entonces, existen \(x\u2081\) y \(x\u2082\) tales que
\n\begin{align}
\n &x\u2081 \u2208 s \tag{1} \\
\n &f(x\u2081) = y \tag{2} \\
\n &x\u2082 \u2208 t \tag{3} \\
\n &f(x\u2082) = y \tag{4}
\n\end{align}
\nDe (2) y (4) se tiene que
\n\[ f(x\u2081) = f(x\u2082) \]
\ny, por ser \(f\) inyectiva, se tiene que
\n\[ x\u2081 = x\u2082 \]
\ny, por (1), se tiene que
\n\[ x\u2082 \u2208 t \]
\ny, por (3), se tiene que
\n\[ x\u2082 \u2208 s \u2229 t \]
\nPor tanto,
\n\[ f(x\u2082) \u2208 f[s \u2229 t] \]
\ny, por (4),
\n\[ y \u2208 f[s \u2229 t] \]<\/p>\n
2. Demostraciones con Lean4<\/h2>\n\nimport Mathlib.Data.Set.Function\n\nopen Set Function\n\nvariable {\u03b1 \u03b2 : Type _}\nvariable (f : \u03b1 \u2192 \u03b2)\nvariable (s t : Set \u03b1)\n\n-- 1\u00aa demostraci\u00f3n\n-- ===============\n\nexample\n (h : Injective f)\n : f '' s \u2229 f '' t \u2286 f '' (s \u2229 t) :=\nby\n intros y hy\n -- y : \u03b2\n -- hy : y \u2208 f '' s \u2229 f '' t\n -- \u22a2 y \u2208 f '' (s \u2229 t)\n rcases hy with \u27e8hy1, hy2\u27e9\n -- hy1 : y \u2208 f '' s\n -- hy2 : y \u2208 f '' t\n rcases hy1 with \u27e8x1, hx1\u27e9\n -- x1 : \u03b1\n -- hx1 : x1 \u2208 s \u2227 f x1 = y\n rcases hx1 with \u27e8x1s, fx1y\u27e9\n -- x1s : x1 \u2208 s\n -- fx1y : f x1 = y\n rcases hy2 with \u27e8x2, hx2\u27e9\n -- x2 : \u03b1\n -- hx2 : x2 \u2208 t \u2227 f x2 = y\n rcases hx2 with \u27e8x2t, fx2y\u27e9\n -- x2t : x2 \u2208 t\n -- fx2y : f x2 = y\n have h1 : f x1 = f x2 := Eq.trans fx1y fx2y.symm\n have h2 : x1 = x2 := h (congrArg f (h h1))\n have h3 : x2 \u2208 s := by rwa [h2] at x1s\n have h4 : x2 \u2208 s \u2229 t := by exact \u27e8h3, x2t\u27e9\n have h5 : f x2 \u2208 f '' (s \u2229 t) := mem_image_of_mem f h4\n show y \u2208 f '' (s \u2229 t)\n rwa [fx2y] at h5\n\n-- 2\u00aa demostraci\u00f3n\n-- ===============\n\nexample\n (h : Injective f)\n : f '' s \u2229 f '' t \u2286 f '' (s \u2229 t) :=\nby\n intros y hy\n -- y : \u03b2\n -- hy : y \u2208 f '' s \u2229 f '' t\n -- \u22a2 y \u2208 f '' (s \u2229 t)\n rcases hy with \u27e8hy1, hy2\u27e9\n -- hy1 : y \u2208 f '' s\n -- hy2 : y \u2208 f '' t\n rcases hy1 with \u27e8x1, hx1\u27e9\n -- x1 : \u03b1\n -- hx1 : x1 \u2208 s \u2227 f x1 = y\n rcases hx1 with \u27e8x1s, fx1y\u27e9\n -- x1s : x1 \u2208 s\n -- fx1y : f x1 = y\n rcases hy2 with \u27e8x2, hx2\u27e9\n -- x2 : \u03b1\n -- hx2 : x2 \u2208 t \u2227 f x2 = y\n rcases hx2 with \u27e8x2t, fx2y\u27e9\n -- x2t : x2 \u2208 t\n -- fx2y : f x2 = y\n use x1\n -- \u22a2 x1 \u2208 s \u2229 t \u2227 f x1 = y\n constructor\n . -- \u22a2 x1 \u2208 s \u2229 t\n constructor\n . -- \u22a2 x1 \u2208 s\n exact x1s\n . -- \u22a2 x1 \u2208 t\n convert x2t\n -- \u22a2 x1 = x2\n apply h\n -- \u22a2 f x1 = f x2\n rw [\u2190 fx2y] at fx1y\n -- fx1y : f x1 = f x2\n exact fx1y\n . -- \u22a2 f x1 = y\n exact fx1y\n\n-- 3\u00aa demostraci\u00f3n\n-- ===============\n\nexample\n (h : Injective f)\n : f '' s \u2229 f '' t \u2286 f '' (s \u2229 t) :=\nby\n rintro y \u27e8\u27e8x1, x1s, fx1y\u27e9, \u27e8x2, x2t, fx2y\u27e9\u27e9\n -- y : \u03b2\n -- x1 : \u03b1\n -- x1s : x1 \u2208 s\n -- fx1y : f x1 = y\n -- x2 : \u03b1\n -- x2t : x2 \u2208 t\n -- fx2y : f x2 = y\n -- \u22a2 y \u2208 f '' (s \u2229 t)\n use x1\n -- \u22a2 x1 \u2208 s \u2229 t \u2227 f x1 = y\n constructor\n . -- \u22a2 x1 \u2208 s \u2229 t\n constructor\n . -- \u22a2 x1 \u2208 s\n exact x1s\n . -- \u22a2 x1 \u2208 t\n convert x2t\n -- \u22a2 x1 = x2\n apply h\n -- \u22a2 f x1 = f x2\n rw [\u2190 fx2y] at fx1y\n -- fx1y : f x1 = f x2\n exact fx1y\n . -- \u22a2 f x1 = y\n exact fx1y\n<\/pre>\n