Demostrar que si f es inyectiva, entonces<\/p>\n
\n f\u207b\u00b9[f[s]] \u2286 s\n<\/pre>\nPara ello, completar la siguiente teor\u00eda de Lean:<\/p>\n
\nimport data.set.basic\n\nopen set function\n\nvariables {\u03b1 : Type*} {\u03b2 : Type*}\nvariable f : \u03b1 \u2192 \u03b2\nvariable s : set \u03b1\n\nexample\n (h : injective f)\n : f \u207b\u00b9' (f '' s) \u2286 s :=\nsorry\n<\/pre>\n[expand title=\u00bbSoluciones con Lean\u00bb]<\/p>\n
\r\nimport data.set.basic\r\n\r\nopen set function\r\n\r\nvariables {\u03b1 : Type*} {\u03b2 : Type*}\r\nvariable f : \u03b1 \u2192 \u03b2\r\nvariable s : set \u03b1\r\n\r\n-- 1\u00aa demostraci\u00f3n\r\n-- ===============\r\n\r\nexample\r\n (h : injective f)\r\n : f \u207b\u00b9' (f '' s) \u2286 s :=\r\nbegin\r\n intros x hx,\r\n rw mem_preimage at hx,\r\n rw mem_image_eq at hx,\r\n cases hx with y hy,\r\n cases hy with ys fyx,\r\n unfold injective at h,\r\n have h1 : y = x := h fyx,\r\n rw \u2190 h1,\r\n exact ys,\r\nend\r\n\r\n-- 2\u00aa demostraci\u00f3n\r\n-- ===============\r\n\r\nexample\r\n (h : injective f)\r\n : f \u207b\u00b9' (f '' s) \u2286 s :=\r\nbegin\r\n intros x hx,\r\n rw mem_preimage at hx,\r\n rcases hx with \u27e8y, ys, fyx\u27e9,\r\n rw \u2190 h fyx,\r\n exact ys,\r\nend\r\n\r\n-- 3\u00aa demostraci\u00f3n\r\n-- ===============\r\n\r\nexample\r\n (h : injective f)\r\n : f \u207b\u00b9' (f '' s) \u2286 s :=\r\nbegin\r\n rintros x \u27e8y, ys, hy\u27e9,\r\n rw \u2190 h hy,\r\n exact ys,\r\nend\r\n<\/pre>\n