{"id":1724,"date":"2023-10-24T06:00:30","date_gmt":"2023-10-24T04:00:30","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/?p=1724"},"modified":"2023-10-18T18:03:11","modified_gmt":"2023-10-18T16:03:11","slug":"24-oct-23","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/24-oct-23\/","title":{"rendered":"La funci\u00f3n (x \u21a6 x + c) es inyectiva"},"content":{"rendered":"

Demostrar con Lean4 que la funci\u00f3n \(x \u21a6 x + c\) es inyectiva.<\/p>\n

Para ello, completar la siguiente teor\u00eda de Lean4:<\/p>\n

\nimport Mathlib.Data.Real.Basic\nopen Function\n\nvariable {c : \u211d}\n\nexample : Injective ((. + c)) :=\nby sorry\n<\/pre>\n
<\/p>\n
Demostraci\u00f3n en lenguaje natural<\/b><\/p>\n

\nSe usar\u00e1 el lema
\n\[ (\u2200 a, b, c) [a + b = c + b \u2192 a = c] \tag{L1} \]<\/p>\n
Hay que demostrar que
\n\[ (\u2200 x\u2081, x\u2082) [f(x\u2081) = f(x\u2082) \u2192 x\u2081 = x\u2082] \]
\nSean \(x\u2081, x\u2082\) tales que \(f(x\u2081) = f(x\u2082)\). Entonces,
\n\[ x\u2081 + c = x\u2082 + c \]
\ny, por L1, \(x\u2081 = x\u2082\).<\/p>\n
Demostraciones con Lean4<\/b><\/p>\n
\nimport Mathlib.Data.Real.Basic\nopen Function\n\nvariable {c : \u211d}\n\n-- 1\u00aa demostraci\u00f3n\nexample : Injective ((. + c)) :=\nby\n  intro (x1 : \u211d) (x2 : \u211d) (h1 : x1 + c = x2 + c)\n  show x1 = x2\n  exact add_right_cancel h1\n\n-- 2\u00aa demostraci\u00f3n\nexample : Injective ((. + c)) :=\nby\n  intro x1 x2 h1\n  show x1 = x2\n  exact add_right_cancel h1\n\n-- 3\u00aa demostraci\u00f3n\nexample : Injective ((. + c)) :=\n  fun _ _ h \u21a6 add_right_cancel h\n\n-- Lemas usados\n-- ============\n\n-- variable {a b : \u211d}\n-- #check (add_right_cancel : a + b = c + b \u2192 a = c)\n<\/pre>\n
Demostraciones interactivas<\/b><\/p>\n
Se puede interactuar con las demostraciones anteriores en Lean 4 Web<\/a>.<\/p>\n
Referencias<\/b><\/p>\n