En Lean, que g es una inversa por la izquierda de f est\u00e1 definido por<\/p>\n
\n left_inverse (g : \u03b2 \u2192 \u03b1) (f : \u03b1 \u2192 \u03b2) : Prop :=\n \u2200 x, g (f x) = x\n<\/pre>\ny que f tenga inversa por la izquierda est\u00e1 definido por<\/p>\n
\n has_left_inverse (f : \u03b1 \u2192 \u03b2) : Prop :=\n \u2203 finv : \u03b2 \u2192 \u03b1, left_inverse finv f\n<\/pre>\nFinalmente, que f es inyectiva est\u00e1 definido por<\/p>\n
\n injective (f : \u03b1 \u2192 \u03b2) : Prop :=\n \u2200 \u2983x y\u2984, f x = f y \u2192 x = y\n<\/pre>\nDemostrar que si f es una funci\u00f3n inyectiva con dominio no vac\u00edo, entonces f tiene inversa por la izquierda.<\/p>\n
Para ello, completar la siguiente teor\u00eda de Lean:<\/p>\n
\nimport tactic\nopen function classical\n\nvariables {\u03b1 \u03b2: Type*}\nvariable {f : \u03b1 \u2192 \u03b2}\n\n-- 1\u00aa demostraci\u00f3n\nexample\n [h\u03b1 : nonempty \u03b1]\n (hf : injective f)\n : has_left_inverse f :=\nsorry\n<\/pre>\n[expand title=\u00bbSoluciones con Lean\u00bb]<\/p>\n
\r\nimport tactic\r\nopen function classical\r\n\r\nvariables {\u03b1 \u03b2: Type*}\r\nvariable {f : \u03b1 \u2192 \u03b2}\r\n\r\n-- 1\u00aa demostraci\u00f3n\r\nexample\r\n [h\u03b1 : nonempty \u03b1]\r\n (hf : injective f)\r\n : has_left_inverse f :=\r\nbegin\r\n classical,\r\n unfold has_left_inverse,\r\n let g := \u03bb y, if h : \u2203 x, f x = y then some h else choice h\u03b1,\r\n use g,\r\n unfold left_inverse,\r\n intro a,\r\n have h1 : \u2203 x : \u03b1, f x = f a := Exists.intro a rfl,\r\n dsimp at *,\r\n dsimp [g],\r\n rw dif_pos h1,\r\n apply hf,\r\n exact some_spec h1,\r\nend\r\n\r\n-- 2\u00aa demostraci\u00f3n\r\nexample\r\n [h\u03b1 : nonempty \u03b1]\r\n (hf : injective f)\r\n : has_left_inverse f :=\r\nbegin\r\n classical,\r\n let g := \u03bb y, if h : \u2203 x, f x = y then some h else choice h\u03b1,\r\n use g,\r\n intro a,\r\n have h1 : \u2203 x : \u03b1, f x = f a := Exists.intro a rfl,\r\n dsimp [g],\r\n rw dif_pos h1,\r\n exact hf (some_spec h1),\r\nend\r\n\r\n-- 3\u00aa demostraci\u00f3n\r\nexample\r\n [h\u03b1 : nonempty \u03b1]\r\n (hf : injective f)\r\n : has_left_inverse f :=\r\nbegin\r\n unfold has_left_inverse,\r\n use inv_fun f,\r\n unfold left_inverse,\r\n intro x,\r\n apply hf,\r\n apply inv_fun_eq,\r\n use x,\r\nend\r\n\r\n-- 4\u00aa demostraci\u00f3n\r\nexample\r\n [h\u03b1 : nonempty \u03b1]\r\n (hf : injective f)\r\n : has_left_inverse f :=\r\nbegin\r\n use inv_fun f,\r\n intro x,\r\n apply hf,\r\n apply inv_fun_eq,\r\n use x,\r\nend\r\n\r\n-- 5\u00aa demostraci\u00f3n\r\nexample\r\n [h\u03b1 : nonempty \u03b1]\r\n (hf : injective f)\r\n : has_left_inverse f :=\r\n\u27e8inv_fun f, left_inverse_inv_fun hf\u27e9\r\n\r\n-- 6\u00aa demostraci\u00f3n\r\nexample\r\n [h\u03b1 : nonempty \u03b1]\r\n (hf : injective f)\r\n : has_left_inverse f :=\r\ninjective.has_left_inverse hf\r\n<\/pre>\n