Demostrar que<\/p>\n
\n f[f\u00b9[u]] \u2286 u\n<\/pre>\nPara ello, completar la siguiente teor\u00eda de Lean:<\/p>\n
\nimport data.set.basic\nopen set\n\nvariables {\u03b1 : Type*} {\u03b2 : Type*}\nvariable f : \u03b1 \u2192 \u03b2\nvariable u : set \u03b2\n\nexample : f '' (f\u207b\u00b9' u) \u2286 u :=\nsorry\n<\/pre>\n[expand title=\u00bbSoluciones con Lean\u00bb]<\/p>\n
\r\nimport data.set.basic\r\nopen set\r\n\r\nvariables {\u03b1 : Type*} {\u03b2 : Type*}\r\nvariable f : \u03b1 \u2192 \u03b2\r\nvariable u : set \u03b2\r\n\r\n-- 1\u00aa demostraci\u00f3n\r\n-- ===============\r\n\r\nexample : f '' (f\u207b\u00b9' u) \u2286 u :=\r\nbegin\r\n intros y h,\r\n cases h with x h2,\r\n cases h2 with hx fxy,\r\n rw \u2190 fxy,\r\n exact hx,\r\nend\r\n\r\n-- 2\u00aa demostraci\u00f3n\r\n-- ===============\r\n\r\nexample : f '' (f\u207b\u00b9' u) \u2286 u :=\r\nbegin\r\n intros y h,\r\n rcases h with \u27e8x, hx, fxy\u27e9,\r\n rw \u2190 fxy,\r\n exact hx,\r\nend\r\n\r\n-- 3\u00aa demostraci\u00f3n\r\n-- ===============\r\n\r\nexample : f '' (f\u207b\u00b9' u) \u2286 u :=\r\nbegin\r\n rintros y \u27e8x, hx, fxy\u27e9,\r\n rw \u2190 fxy,\r\n exact hx,\r\nend\r\n\r\n-- 4\u00aa demostraci\u00f3n\r\n-- ===============\r\n\r\nexample : f '' (f\u207b\u00b9' u) \u2286 u :=\r\nbegin\r\n rintros y \u27e8x, hx, rfl\u27e9,\r\n exact hx,\r\nend\r\n\r\n-- 5\u00aa demostraci\u00f3n\r\n-- ===============\r\n\r\nexample : f '' (f\u207b\u00b9' u) \u2286 u :=\r\nimage_preimage_subset f u\r\n\r\n-- 6\u00aa demostraci\u00f3n\r\n-- ===============\r\n\r\nexample : f '' (f\u207b\u00b9' u) \u2286 u :=\r\nby simp\r\n<\/pre>\n