Demostrar que<\/p>\n
\n s \u222a f\u207b\u00b9[v] \u2286 f\u00b9[f[s] \u222a 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\nvariable s : set \u03b1\nvariable v : set \u03b2\n\nexample : s \u222a f \u207b\u00b9' v \u2286 f \u207b\u00b9' (f '' s \u222a 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\nvariable s : set \u03b1\r\nvariable v : set \u03b2\r\n\r\n-- 1\u00aa demostraci\u00f3n\r\n-- ===============\r\n\r\nexample : s \u222a f \u207b\u00b9' v \u2286 f \u207b\u00b9' (f '' s \u222a v) :=\r\nbegin\r\n intros x hx,\r\n rw mem_preimage,\r\n cases hx with xs xv,\r\n { apply mem_union_left,\r\n apply mem_image_of_mem,\r\n exact xs, },\r\n { apply mem_union_right,\r\n rw \u2190 mem_preimage,\r\n exact xv, },\r\nend\r\n\r\n-- 2\u00aa demostraci\u00f3n\r\n-- ===============\r\n\r\nexample : s \u222a f \u207b\u00b9' v \u2286 f \u207b\u00b9' (f '' s \u222a v) :=\r\nbegin\r\n intros x hx,\r\n cases hx with xs xv,\r\n { apply mem_union_left,\r\n apply mem_image_of_mem,\r\n exact xs, },\r\n { apply mem_union_right,\r\n exact xv, },\r\nend\r\n\r\n-- 3\u00aa demostraci\u00f3n\r\n-- ===============\r\n\r\nexample : s \u222a f \u207b\u00b9' v \u2286 f \u207b\u00b9' (f '' s \u222a v) :=\r\nbegin\r\n rintros x (xs | xv),\r\n { left,\r\n exact mem_image_of_mem f xs, },\r\n { right,\r\n exact xv, },\r\nend\r\n\r\n-- 4\u00aa demostraci\u00f3n\r\n-- ===============\r\n\r\nexample : s \u222a f \u207b\u00b9' v \u2286 f \u207b\u00b9' (f '' s \u222a v) :=\r\nbegin\r\n rintros x (xs | xv),\r\n { exact or.inl (mem_image_of_mem f xs), },\r\n { exact or.inr xv, },\r\nend\r\n\r\n-- 5\u00aa demostraci\u00f3n\r\n-- ===============\r\n\r\nexample : s \u222a f \u207b\u00b9' v \u2286 f \u207b\u00b9' (f '' s \u222a v) :=\r\nbegin\r\n intros x h,\r\n exact or.elim h (\u03bb xs, or.inl (mem_image_of_mem f xs)) or.inr,\r\nend\r\n\r\n-- 6\u00aa demostraci\u00f3n\r\n-- ===============\r\n\r\nexample : s \u222a f \u207b\u00b9' v \u2286 f \u207b\u00b9' (f '' s \u222a v) :=\r\n\u03bb x h, or.elim h (\u03bb xs, or.inl (mem_image_of_mem f xs)) or.inr\r\n\r\n-- 7\u00aa demostraci\u00f3n\r\n-- ===============\r\n\r\nexample : s \u222a f \u207b\u00b9' v \u2286 f \u207b\u00b9' (f '' s \u222a v) :=\r\nbegin\r\n rintros x (xs | xv),\r\n { show f x \u2208 f '' s \u222a v,\r\n use [x, xs, rfl] },\r\n { show f x \u2208 f '' s \u222a v,\r\n right,\r\n apply xv },\r\nend\r\n\r\n-- 8\u00aa demostraci\u00f3n\r\n-- ===============\r\n\r\nexample : s \u222a f \u207b\u00b9' v \u2286 f \u207b\u00b9' (f '' s \u222a v) :=\r\nunion_preimage_subset s v f\r\n<\/pre>\n