Demostrar que la composici\u00f3n de dos funciones inyectivas es una funci\u00f3n inyectiva.<\/p>\n
Para ello, completar la siguiente teor\u00eda de Lean:<\/p>\n
\nimport tactic\nopen function\n\nvariables {X Y Z : Type}\nvariable {f : X \u2192 Y}\nvariable {g : Y \u2192 Z}\n\nexample\n (Hf : injective f)\n (Hg : injective g)\n : injective (g \u2218 f) :=\nsorry\n<\/pre>\n[expand title=\u00bbSoluciones con Lean\u00bb]<\/p>\n
\r\nimport tactic\r\nopen function\r\n\r\nvariables {X Y Z : Type}\r\nvariable {f : X \u2192 Y}\r\nvariable {g : Y \u2192 Z}\r\n\r\n-- 1\u00aa demostraci\u00f3n\r\nexample\r\n (Hf : injective f)\r\n (Hg : injective g)\r\n : injective (g \u2218 f) :=\r\nbegin\r\n intros x y h,\r\n apply Hf,\r\n apply Hg,\r\n exact h,\r\nend\r\n\r\n-- 2\u00aa demostraci\u00f3n\r\nexample\r\n (Hf : injective f)\r\n (Hg : injective g)\r\n : injective (g \u2218 f) :=\r\nbegin\r\n intros x y h,\r\n apply Hf,\r\n exact Hg h,\r\nend\r\n\r\n-- 3\u00aa demostraci\u00f3n\r\nexample\r\n (Hf : injective f)\r\n (Hg : injective g)\r\n : injective (g \u2218 f) :=\r\nbegin\r\n intros x y h,\r\n exact Hf (Hg h),\r\nend\r\n\r\n-- 4\u00aa demostraci\u00f3n\r\nexample\r\n (Hf : injective f)\r\n (Hg : injective g)\r\n : injective (g \u2218 f) :=\r\n\u03bb x y h, Hf (Hg h)\r\n\r\n-- 5\u00aa demostraci\u00f3n\r\nexample\r\n (Hf : injective f)\r\n (Hg : injective g)\r\n : injective (g \u2218 f) :=\r\nassume x y,\r\nassume h1 : (g \u2218 f) x = (g \u2218 f) y,\r\nhave h2 : f x = f y, from Hg h1,\r\nshow x = y, from Hf h2\r\n\r\n-- 6\u00aa demostraci\u00f3n\r\nexample\r\n (Hf : injective f)\r\n (Hg : injective g)\r\n : injective (g \u2218 f) :=\r\nassume x y,\r\nassume h1 : (g \u2218 f) x = (g \u2218 f) y,\r\nshow x = y, from Hf (Hg h1)\r\n\r\n-- 7\u00aa demostraci\u00f3n\r\nexample\r\n (Hf : injective f)\r\n (Hg : injective g)\r\n : injective (g \u2218 f) :=\r\nassume x y,\r\nassume h1 : (g \u2218 f) x = (g \u2218 f) y,\r\nHf (Hg h1)\r\n\r\n-- 8\u00aa demostraci\u00f3n\r\nexample\r\n (Hf : injective f)\r\n (Hg : injective g)\r\n : injective (g \u2218 f) :=\r\n\u03bb x y h1, Hf (Hg h1)\r\n\r\n-- 9\u00aa demostraci\u00f3n\r\nexample\r\n (Hg : injective g)\r\n (Hf : injective f)\r\n : injective (g \u2218 f) :=\r\n-- by library_search\r\ninjective.comp Hg Hf\r\n\r\n-- 10\u00aa demostraci\u00f3n\r\nexample\r\n (Hg : injective g)\r\n (Hf : injective f)\r\n : injective (g \u2218 f) :=\r\n-- by hint\r\nby tauto\r\n<\/pre>\n