Demostrar con Lean4 que si \(u \u2286 v\), entonces \(f\u207b\u00b9[u] \u2286 f\u207b\u00b9[v]\).<\/p>\n
Para ello, completar la siguiente teor\u00eda de Lean4:<\/p>\n
\nimport Mathlib.Data.Set.Function\nopen Set\n\nvariable {\u03b1 \u03b2 : Type _}\nvariable (f : \u03b1 \u2192 \u03b2)\nvariable (u v : Set \u03b2)\n\nexample\n (h : u \u2286 v)\n : f \u207b\u00b9' u \u2286 f \u207b\u00b9' v :=\nby sorry\n<\/pre>\n<\/p>\n
1. Demostraci\u00f3n en lenguaje natural<\/h2>\n
Por la siguiente cadena de implicaciones:
\n\begin{align}
\n x \u2208 f\u207b\u00b9[u] &\u27f9 f(x) \u2208 u \\
\n &\u27f9 f(x) \u2208 v &&\text{[porque \(u \u2286 v\)]} \\
\n &\u27f9 x \u2208 f\u207b\u00b9[v]
\n\end{align}<\/p>\n
2. Demostraciones con Lean4<\/h2>\n\nimport Mathlib.Data.Set.Function\nopen Set\n\nvariable {\u03b1 \u03b2 : Type _}\nvariable (f : \u03b1 \u2192 \u03b2)\nvariable (u v : Set \u03b2)\n\n-- 1\u00aa demostraci\u00f3n\n-- ===============\n\nexample\n (h : u \u2286 v)\n : f \u207b\u00b9' u \u2286 f \u207b\u00b9' v :=\nby\n intros x hx\n -- x : \u03b1\n -- hx : x \u2208 f \u207b\u00b9' u\n -- \u22a2 x \u2208 f \u207b\u00b9' v\n have h1 : f x \u2208 u := mem_preimage.mp hx\n have h2 : f x \u2208 v := h h1\n show x \u2208 f \u207b\u00b9' v\n exact mem_preimage.mpr h2\n\n-- 2\u00aa demostraci\u00f3n\n-- ===============\n\nexample\n (h : u \u2286 v)\n : f \u207b\u00b9' u \u2286 f \u207b\u00b9' v :=\nby\n intros x hx\n -- x : \u03b1\n -- hx : x \u2208 f \u207b\u00b9' u\n -- \u22a2 x \u2208 f \u207b\u00b9' v\n apply mem_preimage.mpr\n -- \u22a2 f x \u2208 v\n apply h\n -- \u22a2 f x \u2208 u\n apply mem_preimage.mp\n -- \u22a2 x \u2208 f \u207b\u00b9' u\n exact hx\n\n-- 3\u00aa demostraci\u00f3n\n-- ===============\n\nexample\n (h : u \u2286 v)\n : f \u207b\u00b9' u \u2286 f \u207b\u00b9' v :=\nby\n intros x hx\n -- x : \u03b1\n -- hx : x \u2208 f \u207b\u00b9' u\n -- \u22a2 x \u2208 f \u207b\u00b9' v\n apply h\n -- \u22a2 f x \u2208 u\n exact hx\n\n-- 4\u00aa demostraci\u00f3n\n-- ===============\n\nexample\n (h : u \u2286 v)\n : f \u207b\u00b9' u \u2286 f \u207b\u00b9' v :=\nby\n intros x hx\n -- x : \u03b1\n -- hx : x \u2208 f \u207b\u00b9' u\n -- \u22a2 x \u2208 f \u207b\u00b9' v\n exact h hx\n\n-- 5\u00aa demostraci\u00f3n\n-- ===============\n\nexample\n (h : u \u2286 v)\n : f \u207b\u00b9' u \u2286 f \u207b\u00b9' v :=\nfun _ hx \u21a6 h hx\n\n-- 6\u00aa demostraci\u00f3n\n-- ===============\n\nexample\n (h : u \u2286 v)\n : f \u207b\u00b9' u \u2286 f \u207b\u00b9' v :=\nby intro x; apply h\n\n-- 7\u00aa demostraci\u00f3n\n-- ===============\n\nexample\n (h : u \u2286 v)\n : f \u207b\u00b9' u \u2286 f \u207b\u00b9' v :=\npreimage_mono h\n\n-- 8\u00aa demostraci\u00f3n\n-- ===============\n\nexample\n (h : u \u2286 v)\n : f \u207b\u00b9' u \u2286 f \u207b\u00b9' v :=\nby tauto\n\n-- Lemas usados\n-- ============\n\n-- variable (a : \u03b1)\n-- #check (mem_preimage : a \u2208 f \u207b\u00b9' u \u2194 f a \u2208 u)\n-- #check (preimage_mono : u \u2286 v \u2192 f \u207b\u00b9' u \u2286 f \u207b\u00b9' v)\n<\/pre>\n