Demostrar con Lean4 que
\n\[ s \u222a f\u207b\u00b9[v] \u2286 f\u207b\u00b9[f[s] \u222a v] \]<\/p>\n
Para ello, completar la siguiente teor\u00eda de Lean4:<\/p>\n
\nimport Mathlib.Data.Set.Function\n\nopen Set\n\nvariable {\u03b1 \u03b2 : Type _}\nvariable (f : \u03b1 \u2192 \u03b2)\nvariable (s : Set \u03b1)\nvariable (v : Set \u03b2)\n\nexample : s \u222a f \u207b\u00b9' v \u2286 f \u207b\u00b9' (f '' s \u222a v) :=\nby sorry\n<\/pre>\n<\/p>\n
1. Demostraci\u00f3n en lenguaje natural<\/h2>\n
Sea \(x \u2208 s \u222a f\u207b\u00b9[v]\). Entonces, se pueden dar dos casos.<\/p>\n
Caso 1: Supongamos que \(x \u2208 s\). Entonces, se tiene
\n\begin{align}
\n &f(x) \u2208 f[s] \\
\n &f(x) \u2208 f[s] \u222a v \\
\n &x \u2208 f\u207b\u00b9[f[s] \u222a v]
\n\end{align}<\/p>\n
Caso 2: Supongamos que x \u2208 f\u207b\u00b9[v]. Entonces, se tiene
\n\begin{align}
\n &f(x) \u2208 v \\
\n &f(x) \u2208 f[s] \u222a v \\
\n &x \u2208 f\u207b\u00b9[f[s] \u222a v]
\n\end{align}<\/p>\n
2. Demostraciones con Lean4<\/h2>\n\nimport Mathlib.Data.Set.Function\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 : s \u222a f \u207b\u00b9' v \u2286 f \u207b\u00b9' (f '' s \u222a v) :=\nby\n intros x hx\n -- x : \u03b1\n -- hx : x \u2208 s \u222a f \u207b\u00b9' v\n -- \u22a2 x \u2208 f \u207b\u00b9' (f '' s \u222a v)\n cases' hx 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 : f x \u2208 f '' s \u222a v := mem_union_left v h1\n show x \u2208 f \u207b\u00b9' (f '' s \u222a v)\n exact mem_preimage.mpr h2\n . -- xv : x \u2208 f \u207b\u00b9' v\n have h3 : f x \u2208 v := mem_preimage.mp xv\n have h4 : f x \u2208 f '' s \u222a v := mem_union_right (f '' s) h3\n show x \u2208 f \u207b\u00b9' (f '' s \u222a v)\n exact mem_preimage.mpr h4\n\n-- 2\u00aa demostraci\u00f3n\n-- ===============\n\nexample : s \u222a f \u207b\u00b9' v \u2286 f \u207b\u00b9' (f '' s \u222a v) :=\nby\n intros x hx\n -- x : \u03b1\n -- hx : x \u2208 s \u222a f \u207b\u00b9' v\n -- \u22a2 x \u2208 f \u207b\u00b9' (f '' s \u222a v)\n rw [mem_preimage]\n -- \u22a2 f x \u2208 f '' s \u222a v\n cases' hx with xs xv\n . -- xs : x \u2208 s\n apply mem_union_left\n -- \u22a2 f x \u2208 f '' s\n apply mem_image_of_mem\n -- \u22a2 x \u2208 s\n exact xs\n . -- xv : x \u2208 f \u207b\u00b9' v\n apply mem_union_right\n -- \u22a2 f x \u2208 v\n rw [\u2190mem_preimage]\n -- \u22a2 x \u2208 f \u207b\u00b9' v\n exact xv\n\n-- 3\u00aa demostraci\u00f3n\n-- ===============\n\nexample : s \u222a f \u207b\u00b9' v \u2286 f \u207b\u00b9' (f '' s \u222a v) :=\nby\n intros x hx\n -- x : \u03b1\n -- hx : x \u2208 s \u222a f \u207b\u00b9' v\n -- \u22a2 x \u2208 f \u207b\u00b9' (f '' s \u222a v)\n cases' hx with xs xv\n . -- xs : x \u2208 s\n rw [mem_preimage]\n -- \u22a2 f x \u2208 f '' s \u222a v\n apply mem_union_left\n -- \u22a2 f x \u2208 f '' s\n apply mem_image_of_mem\n -- \u22a2 x \u2208 s\n exact xs\n . -- \u22a2 x \u2208 f \u207b\u00b9' (f '' s \u222a v)\n rw [mem_preimage]\n -- \u22a2 f x \u2208 f '' s \u222a v\n apply mem_union_right\n -- \u22a2 f x \u2208 v\n exact xv\n\n-- 4\u00aa demostraci\u00f3n\n-- ===============\n\nexample : s \u222a f \u207b\u00b9' v \u2286 f \u207b\u00b9' (f '' s \u222a v) :=\nby\n rintro x (xs | xv)\n -- x : \u03b1\n -- \u22a2 x \u2208 f \u207b\u00b9' (f '' s \u222a v)\n . -- xs : x \u2208 s\n left\n -- \u22a2 f x \u2208 f '' s\n exact mem_image_of_mem f xs\n . -- xv : x \u2208 f \u207b\u00b9' v\n right\n -- \u22a2 f x \u2208 v\n exact xv\n\n-- 5\u00aa demostraci\u00f3n\n-- ===============\n\nexample : s \u222a f \u207b\u00b9' v \u2286 f \u207b\u00b9' (f '' s \u222a v) :=\nby\n rintro x (xs | xv)\n -- x : \u03b1\n -- \u22a2 x \u2208 f \u207b\u00b9' (f '' s \u222a v)\n . -- xs : x \u2208 s\n exact Or.inl (mem_image_of_mem f xs)\n . -- xv : x \u2208 f \u207b\u00b9' v\n exact Or.inr xv\n\n-- 5\u00aa demostraci\u00f3n\n-- ===============\n\nexample : s \u222a f \u207b\u00b9' v \u2286 f \u207b\u00b9' (f '' s \u222a v) :=\nby\n intros x h\n -- x : \u03b1\n -- h : x \u2208 s \u222a f \u207b\u00b9' v\n -- \u22a2 x \u2208 f \u207b\u00b9' (f '' s \u222a v)\n exact Or.elim h (fun xs \u21a6 Or.inl (mem_image_of_mem f xs)) Or.inr\n\n-- 6\u00aa demostraci\u00f3n\n-- ===============\n\nexample : s \u222a f \u207b\u00b9' v \u2286 f \u207b\u00b9' (f '' s \u222a v) :=\nfun _ h \u21a6 Or.elim h (fun xs \u21a6 Or.inl (mem_image_of_mem f xs)) Or.inr\n\n-- 7\u00aa demostraci\u00f3n\n-- ===============\n\nexample : s \u222a f \u207b\u00b9' v \u2286 f \u207b\u00b9' (f '' s \u222a v) :=\nunion_preimage_subset s v f\n\n-- Lemas usados\n-- ============\n\n-- variable (x : \u03b1)\n-- variable (t : Set \u03b1)\n-- variable (a b c : Prop)\n-- #check (Or.elim : a \u2228 b \u2192 (a \u2192 c) \u2192 (b \u2192 c) \u2192 c)\n-- #check (Or.inl : a \u2192 a \u2228 b)\n-- #check (Or.inr : b \u2192 a \u2228 b)\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-- #check (union_preimage_subset s v f : s \u222a f \u207b\u00b9' v \u2286 f \u207b\u00b9' (f '' s \u222a v))\n<\/pre>\n