Demostrar que si f es inyectiva, entonces<\/p>\n
\n (\u22c2 i, f[A i]) \u2286 f[\u22c2 i, A i]\n<\/pre>\nPara ello, completar la siguiente teor\u00eda de Lean:<\/p>\n
\nimport data.set.basic\nimport tactic\n\nopen set function\n\nvariables {\u03b1 : Type*} {\u03b2 : Type*} {I : Type*}\nvariable f : \u03b1 \u2192 \u03b2\nvariables A : I \u2192 set \u03b1\n\nexample\n (i : I)\n (injf : injective f)\n : (\u22c2 i, f '' A i) \u2286 f '' (\u22c2 i, A i) :=\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 function\r\n\r\nvariables {\u03b1 : Type*} {\u03b2 : Type*} {I : Type*}\r\nvariable f : \u03b1 \u2192 \u03b2\r\nvariables A : I \u2192 set \u03b1\r\n\r\n-- 1\u00aa demostraci\u00f3n\r\n-- ===============\r\n\r\nexample\r\n (i : I)\r\n (injf : injective f)\r\n : (\u22c2 i, f '' A i) \u2286 f '' (\u22c2 i, A i) :=\r\nbegin\r\n intros y hy,\r\n rw mem_Inter at hy,\r\n rcases hy i with \u27e8x, xAi, fxy\u27e9,\r\n use x,\r\n split,\r\n { apply mem_Inter_of_mem,\r\n intro j,\r\n rcases hy j with \u27e8z, zAj, fzy\u27e9,\r\n convert zAj,\r\n apply injf,\r\n rw fxy,\r\n rw \u2190 fzy, },\r\n { exact fxy, },\r\nend\r\n\r\n-- 2\u00aa demostraci\u00f3n\r\n-- ===============\r\n\r\nexample\r\n (i : I)\r\n (injf : injective f)\r\n : (\u22c2 i, f '' A i) \u2286 f '' (\u22c2 i, A i) :=\r\nbegin\r\n intro y,\r\n simp,\r\n intro h,\r\n rcases h i with \u27e8x, xAi, fxy\u27e9,\r\n use x,\r\n split,\r\n { intro j,\r\n rcases h j with \u27e8z, zAi, fzy\u27e9,\r\n have : f x = f z, by rw [fxy, fzy],\r\n have : x = z, from injf this,\r\n rw this,\r\n exact zAi, },\r\n { exact fxy, },\r\nend\r\n<\/pre>\n