Demostrar que<\/p>\n
\n f\u207b\u00b9[u \u222a v] = f\u207b\u00b9[u] \u222a f\u207b\u00b9[v]\n<\/pre>\nPara ello, completar la siguiente teor\u00eda de Lean:<\/p>\n
\nimport data.set.basic\n\nopen set\n\nvariables {\u03b1 : Type*} {\u03b2 : Type*}\nvariable f : \u03b1 \u2192 \u03b2\nvariables u v : set \u03b2\n\nexample : f \u207b\u00b9' (u \u222a v) = f \u207b\u00b9' u \u222a f \u207b\u00b9' v :=\nsorry\n<\/pre>\n[expand title=\u00bbSoluciones con Lean\u00bb]<\/p>\n
\r\nimport data.set.basic\r\n\r\nopen set\r\n\r\nvariables {\u03b1 : Type*} {\u03b2 : Type*}\r\nvariable f : \u03b1 \u2192 \u03b2\r\nvariables u v : set \u03b2\r\n\r\n-- 1\u00aa demostraci\u00f3n\r\n-- ===============\r\n\r\nexample : f \u207b\u00b9' (u \u222a v) = f \u207b\u00b9' u \u222a f \u207b\u00b9' v :=\r\nbegin\r\n ext x,\r\n split,\r\n { intros h,\r\n rw mem_preimage at h,\r\n cases h with fxu fxv,\r\n { left,\r\n apply mem_preimage.mpr,\r\n exact fxu, },\r\n { right,\r\n apply mem_preimage.mpr,\r\n exact fxv, }},\r\n { intro h,\r\n rw mem_preimage,\r\n cases h with xfu xfv,\r\n { rw mem_preimage at xfu,\r\n left,\r\n exact xfu, },\r\n { rw mem_preimage at xfv,\r\n right,\r\n exact xfv, }},\r\nend\r\n\r\n-- 2\u00aa demostraci\u00f3n\r\n-- ===============\r\n\r\nexample : f \u207b\u00b9' (u \u222a v) = f \u207b\u00b9' u \u222a f \u207b\u00b9' v :=\r\nbegin\r\n ext x,\r\n split,\r\n { intros h,\r\n cases h with fxu fxv,\r\n { left,\r\n exact fxu, },\r\n { right,\r\n exact fxv, }},\r\n { intro h,\r\n cases h with xfu xfv,\r\n { left,\r\n exact xfu, },\r\n { right,\r\n exact xfv, }},\r\nend\r\n\r\n-- 3\u00aa demostraci\u00f3n\r\n-- ===============\r\n\r\nexample : f \u207b\u00b9' (u \u222a v) = f \u207b\u00b9' u \u222a f \u207b\u00b9' v :=\r\nbegin\r\n ext x,\r\n split,\r\n { rintro (fxu | fxv),\r\n { exact or.inl fxu, },\r\n { exact or.inr fxv, }},\r\n { rintro (xfu | xfv),\r\n { exact or.inl xfu, },\r\n { exact or.inr xfv, }},\r\nend\r\n\r\n-- 4\u00aa demostraci\u00f3n\r\n-- ===============\r\n\r\nexample : f \u207b\u00b9' (u \u222a v) = f \u207b\u00b9' u \u222a f \u207b\u00b9' v :=\r\nbegin\r\n ext x,\r\n split,\r\n { finish, },\r\n { finish, } ,\r\nend\r\n\r\n-- 5\u00aa demostraci\u00f3n\r\n-- ===============\r\n\r\nexample : f \u207b\u00b9' (u \u222a v) = f \u207b\u00b9' u \u222a f \u207b\u00b9' v :=\r\nbegin\r\n ext x,\r\n finish,\r\nend\r\n\r\n-- 6\u00aa demostraci\u00f3n\r\n-- ===============\r\n\r\nexample : f \u207b\u00b9' (u \u222a v) = f \u207b\u00b9' u \u222a f \u207b\u00b9' v :=\r\nby ext; finish\r\n\r\n-- 7\u00aa demostraci\u00f3n\r\n-- ===============\r\n\r\nexample : f \u207b\u00b9' (u \u222a v) = f \u207b\u00b9' u \u222a f \u207b\u00b9' v :=\r\nby ext; refl\r\n\r\n-- 8\u00aa demostraci\u00f3n\r\n-- ===============\r\n\r\nexample : f \u207b\u00b9' (u \u222a v) = f \u207b\u00b9' u \u222a f \u207b\u00b9' v :=\r\nrfl\r\n\r\n-- 9\u00aa demostraci\u00f3n\r\n-- ===============\r\n\r\nexample : f \u207b\u00b9' (u \u222a v) = f \u207b\u00b9' u \u222a f \u207b\u00b9' v :=\r\npreimage_union\r\n\r\n-- 10\u00aa demostraci\u00f3n\r\n-- ===============\r\n\r\nexample : f \u207b\u00b9' (u \u222a v) = f \u207b\u00b9' u \u222a f \u207b\u00b9' v :=\r\nby simp\r\n<\/pre>\n