Demostrar con Lean4 que si \(f\) es inyectiva, entonces \(f\u207b\u00b9[f[s]\u200b] \u2286 s\).<\/p>\n
Para ello, completar la siguiente teor\u00eda de Lean4:<\/p>\n
\nimport Mathlib.Data.Set.Function\nopen Set Function\nvariable {\u03b1 \u03b2 : Type _}\nvariable (f : \u03b1 \u2192 \u03b2)\nvariable (s : Set \u03b1)\n\nexample\n (h : Injective f)\n : f \u207b\u00b9' (f '' s) \u2286 s :=\nby sorry\n<\/pre>\n<\/p>\n
1. Demostraci\u00f3n en lenguaje natural<\/h2>\n
Sea \(x\) tal que
\n\[ x \u2208 f\u207b\u00b9[f[s]] \]
\nEntonces,
\n\[ f(x) \u2208 f[s] \]
\ny, por tanto, existe un
\n\[ y \u2208 s \tag{1} \]
\ntal que
\n\[ f(y) = f(x) \tag{2} \]
\nDe (2), puesto que \(f\) es inyectiva, se tiene que
\n\[ y = x \tag{3} \]
\nFinalmente, de (3) y (1), se tiene que
\n\[ x \u2208 s \]
\nque es lo que ten\u00edamos que demostrar.<\/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 : Set \u03b1)\n\n-- 1\u00aa demostraci\u00f3n\n-- ===============\n\nexample\n (h : Injective f)\n : f \u207b\u00b9' (f '' s) \u2286 s :=\nby\n intros x hx\n -- x : \u03b1\n -- hx : x \u2208 f \u207b\u00b9' (f '' s)\n -- \u22a2 x \u2208 s\n have h1 : f x \u2208 f '' s := mem_preimage.mp hx\n have h2 : \u2203 y, y \u2208 s \u2227 f y = f x := (mem_image f s (f x)).mp h1\n obtain \u27e8y, hy : y \u2208 s \u2227 f y = f x\u27e9 := h2\n obtain \u27e8ys : y \u2208 s, fyx : f y = f x\u27e9 := hy\n have h3 : y = x := h fyx\n show x \u2208 s\n exact h3 \u25b8 ys\n\n-- 2\u00aa demostraci\u00f3n\n-- ===============\n\nexample\n (h : Injective f)\n : f \u207b\u00b9' (f '' s) \u2286 s :=\nby\n intros x hx\n -- x : \u03b1\n -- hx : x \u2208 f \u207b\u00b9' (f '' s)\n -- \u22a2 x \u2208 s\n rw [mem_preimage] at hx\n -- hx : f x \u2208 f '' s\n rw [mem_image] at hx\n -- hx : \u2203 x_1, x_1 \u2208 s \u2227 f x_1 = f x\n rcases hx with \u27e8y, hy\u27e9\n -- y : \u03b1\n -- hy : y \u2208 s \u2227 f y = f x\n rcases hy with \u27e8ys, fyx\u27e9\n -- ys : y \u2208 s\n -- fyx : f y = f x\n unfold Injective at h\n -- h : \u2200 \u2983a\u2081 a\u2082 : \u03b1\u2984, f a\u2081 = f a\u2082 \u2192 a\u2081 = a\u2082\n have h1 : y = x := h fyx\n rw [\u2190h1]\n -- \u22a2 y \u2208 s\n exact ys\n\n-- 3\u00aa demostraci\u00f3n\n-- ===============\n\nexample\n (h : Injective f)\n : f \u207b\u00b9' (f '' s) \u2286 s :=\nby\n intros x hx\n -- x : \u03b1\n -- hx : x \u2208 f \u207b\u00b9' (f '' s)\n -- \u22a2 x \u2208 s\n rw [mem_preimage] at hx\n -- hx : f x \u2208 f '' s\n rcases hx with \u27e8y, ys, fyx\u27e9\n -- y : \u03b1\n -- ys : y \u2208 s\n -- fyx : f y = f x\n rw [\u2190h fyx]\n -- \u22a2 y \u2208 s\n exact ys\n\n-- 4\u00aa demostraci\u00f3n\n-- ===============\n\nexample\n (h : Injective f)\n : f \u207b\u00b9' (f '' s) \u2286 s :=\nby\n rintro x \u27e8y, ys, hy\u27e9\n -- x y : \u03b1\n -- ys : y \u2208 s\n -- hy : f y = f x\n -- \u22a2 x \u2208 s\n rw [\u2190h hy]\n -- \u22a2 y \u2208 s\n exact ys\n\n-- Lemas usados\n-- ============\n\n-- variable (x : \u03b1)\n-- variable (y : \u03b2)\n-- variable (t : Set \u03b2)\n-- #check (mem_image f s y : y \u2208 f '' s \u2194 \u2203 (x : \u03b1), x \u2208 s \u2227 f x = y)\n-- #check (mem_preimage : x \u2208 f \u207b\u00b9' t \u2194 f x \u2208 t)\n<\/pre>\n