Demostrar con Lean4 que si \(c \u2260 0\), entonces la funci\u00f3n \(x \u21a6 cx + d\) es suprayectiva.<\/p>\n
Para ello, completar la siguiente teor\u00eda de Lean4:<\/p>\n
\nimport Mathlib.Data.Real.Basic\nvariable {c d : \u211d}\nopen Function\n\nexample\n (h : c \u2260 0)\n : Surjective (fun x \u21a6 c * x + d) :=\nby sorry\n<\/pre>\n<\/p>\n
Demostraci\u00f3n en lenguaje natural<\/b><\/p>\n
Hay que demostrar que
\n\[ (\u2200x \u2208 \u211d)(\u2203y \u2208 \u211d)[cy+d = x] \]
\nPara \(x \u2208 \u211d\), sea \(y = \dfrac{x-d}{c}\). Entonces,
\n\begin{align}
\n cy &= c\left(\frac{x-d}{c}\right)+d \\
\n &= (x-d)+d \\
\n &= x
\n\end{align}<\/p>\n
Demostraciones con Lean4<\/b><\/p>\n\nimport Mathlib.Data.Real.Basic\nvariable {c d : \u211d}\nopen Function\n\n-- 1\u00aa demostraci\u00f3n\n-- ===============\n\nexample\n (h : c \u2260 0)\n : Surjective (fun x \u21a6 c * x + d) :=\nby\n intro x\n -- x : \u211d\n -- \u22a2 \u2203 a, (fun x => c * x + d) a = x\n use ((x - d) \/ c)\n -- \u22a2 (fun x => c * x + d) ((x - d) \/ c) = x\n dsimp\n -- \u22a2 c * ((x - d) \/ c) + d = x\n show c * ((x - d) \/ c) + d = x\n calc c * ((x - d) \/ c) + d\n = (x - d) + d := congrArg (. + d) (mul_div_cancel' (x - d) h)\n _ = x := sub_add_cancel x d\n\n-- 2\u00aa demostraci\u00f3n\n-- ===============\n\nexample\n (h : c \u2260 0)\n : Surjective (fun x \u21a6 c * x + d) :=\nby\n intro x\n -- x : \u211d\n -- \u22a2 \u2203 a, (fun x => c * x + d) a = x\n use ((x - d) \/ c)\n -- \u22a2 (fun x => c * x + d) ((x - d) \/ c) = x\n dsimp\n -- \u22a2 c * ((x - d) \/ c) + d = x\n simp [mul_div_cancel', h]\n\n-- 3\u00aa demostraci\u00f3n\n-- ===============\n\nexample\n (h : c \u2260 0)\n : Surjective (fun x \u21a6 c * x + d) :=\nby\n intro x\n -- x : \u211d\n -- \u22a2 \u2203 a, (fun x => c * x + d) a = x\n use ((x - d) \/ c)\n -- \u22a2 (fun x => c * x + d) ((x - d) \/ c) = x\n simp [mul_div_cancel', h]\n\n-- 4\u00aa demostraci\u00f3n\n-- ===============\n\nexample\n (h : c \u2260 0)\n : Surjective (fun x \u21a6 c * x + d) :=\nfun x \u21a6 \u27e8(x - d) \/ c, by simp [mul_div_cancel', h]\u27e9\n\n-- Lemas usados\n-- ============\n\n-- variable (a b : \u211d)\n-- #check (mul_div_cancel' a : b \u2260 0 \u2192 b * (a \/ b) = a)\n-- #check (sub_add_cancel a b : a - b + b = a)\n<\/pre>\nDemostraciones interactivas<\/b><\/p>\n
Se puede interactuar con las demostraciones anteriores en Lean 4 Web<\/a>.<\/p>\nReferencias<\/b><\/p>\n