Demostrar con Lean4 que si \(c \u2260 0\), entonces la funci\u00f3n \(x \u21a6 cx\) es inyectiva.<\/p>\n
Para ello, completar la siguiente teor\u00eda de Lean4:<\/p>\n
\nimport Mathlib.Data.Real.Basic\nopen Function\nvariable {c : \u211d}\n\nexample\n (h : c \u2260 0)\n : 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 \u2260 0 \u2192 (ab = ac \u2194 b = 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\[ cx\u2081 = cx\u2082 \]
\ny, por L1 y puesto que \(c \u2260 0\), se tiene que
\n\[ x\u2081 = x\u2082 \]<\/p>\n
Demostraciones con Lean4<\/b><\/p>\n\nimport Mathlib.Data.Real.Basic\nopen Function\nvariable {c : \u211d}\n\n-- 1\u00aa demostraci\u00f3n\nexample\n (h : c \u2260 0)\n : Injective ((c * .)) :=\nby\n intro (x1 : \u211d) (x2 : \u211d) (h1 : c * x1 = c * x2)\n show x1 = x2\n exact (mul_right_inj' h).mp h1\n\n-- 2\u00aa demostraci\u00f3n\nexample\n (h : c \u2260 0)\n : Injective ((c * .)) :=\nfun _ _ h1 \u21a6 mul_left_cancel\u2080 h h1\n\n-- Lemas usados\n-- ============\n\n-- variable (a b : \u211d)\n-- #check (mul_right_inj' : a \u2260 0 \u2192 (a * b = a * c \u2194 b = c))\n-- #check (mul_left_cancel\u2080 : a \u2260 0 \u2192 a * b = a * c \u2192 b = c)\n<\/pre>\nDemostraciones interactivas<\/b><\/p>\n
Se puede interactuar con las demostraciones anteriores en Lean 4 Web<\/a>.<\/p>\nReferencias<\/b><\/p>\n