Demostrar que si s \u2286 t, entonces<\/p>\n
\n f[s] \u2286 f[t]\n<\/pre>\nPara ello, completar la siguiente teor\u00eda de Lean:<\/p>\n
\nimport data.set.basic\nimport tactic\n\nopen set\n\nvariables {\u03b1 : Type*} {\u03b2 : Type*}\nvariable f : \u03b1 \u2192 \u03b2\nvariables s t : set \u03b1\n\nexample\n (h : s \u2286 t)\n : f '' s \u2286 f '' t :=\nsorry\n<\/pre>\n[expand title=\u00bbSoluciones con Lean\u00bb]<\/p>\n
\r\nimport data.set.basic\r\nimport tactic\r\n\r\nopen set\r\n\r\nvariables {\u03b1 : Type*} {\u03b2 : Type*}\r\nvariable f : \u03b1 \u2192 \u03b2\r\nvariables s t : set \u03b1\r\n\r\n-- 1\u00aa demostraci\u00f3n\r\n-- ===============\r\n\r\nexample\r\n (h : s \u2286 t)\r\n : f '' s \u2286 f '' t :=\r\nbegin\r\n intros y hy,\r\n rw mem_image at hy,\r\n cases hy with x hx,\r\n cases hx with xs fxy,\r\n use x,\r\n split,\r\n { exact h xs, },\r\n { exact fxy, },\r\nend\r\n\r\n-- 2\u00aa demostraci\u00f3n\r\n-- ===============\r\n\r\nexample\r\n (h : s \u2286 t)\r\n : f '' s \u2286 f '' t :=\r\nbegin\r\n intros y hy,\r\n rcases hy with \u27e8x, xs, fxy\u27e9,\r\n use x,\r\n exact \u27e8h xs, fxy\u27e9,\r\nend\r\n\r\n-- 3\u00aa demostraci\u00f3n\r\n-- ===============\r\n\r\nexample\r\n (h : s \u2286 t)\r\n : f '' s \u2286 f '' t :=\r\nbegin\r\n rintros y \u27e8x, xs, fxy \u27e9,\r\n use [x, h xs, fxy],\r\nend\r\n\r\n-- 4\u00aa demostraci\u00f3n\r\n-- ===============\r\n\r\nexample\r\n (h : s \u2286 t)\r\n : f '' s \u2286 f '' t :=\r\nby finish [subset_def, mem_image_eq]\r\n\r\n-- 5\u00aa demostraci\u00f3n\r\n-- ===============\r\n\r\nexample\r\n (h : s \u2286 t)\r\n : f '' s \u2286 f '' t :=\r\nimage_subset f h\r\n<\/pre>\n