{"id":1765,"date":"2023-11-09T06:00:35","date_gmt":"2023-11-09T04:00:35","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/?p=1765"},"modified":"2023-10-30T14:18:27","modified_gmt":"2023-10-30T12:18:27","slug":"09-nov-23","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/09-nov-23\/","title":{"rendered":"Si c \u2260 0, entonces la funci\u00f3n (x \u21a6 cx) es suprayectiva"},"content":{"rendered":"

Demostrar con Lean4 que si \(c \u2260 0\), entonces la funci\u00f3n \(x \u21a6 cx\) es suprayectiva.<\/p>\n

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

\nimport Mathlib.Data.Real.Basic\nvariable {c : \u211d}\nopen Function\n\nexample\n  (h : c \u2260 0)\n  : Surjective (fun x \u21a6 c * x) :=\nby sorry\n<\/pre>\n
<\/p>\n
Demostraci\u00f3n en lenguaje natural<\/b><\/p>\n

\nHay que demostrar que
\n\[ (\u2200 x \u2208 \u211d)(\u2203 y \u2208 \u211d)[cy = x] \]
\nSea \(x \u2208 \u211d\). Entonces, \(y = x\/c \u2208 R\) y
\n\begin{align}
\n   cy &= c(x\/c) \\
\n      &= y
\n\end{align}<\/p>\n
Demostraciones con Lean4<\/b><\/p>\n
\nimport Mathlib.Data.Real.Basic\nvariable {c : \u211d}\nopen Function\n\n-- 1\u00aa demostraci\u00f3n\nexample\n  (h : c \u2260 0)\n  : Surjective (fun x \u21a6 c * x) :=\nby\n  intro x\n  -- x : \u211d\n  -- \u22a2 \u2203 a, (fun x => c * x) a = x\n  use (x \/ c)\n  -- \u22a2 (fun x => c * x) (x \/ c) = x\n  dsimp\n  -- \u22a2 c * (x \/ c) = x\n  rw [mul_comm]\n  -- \u22a2 (x \/ c) * c = x\n  exact div_mul_cancel x h\n\n-- 2\u00aa demostraci\u00f3n\nexample\n  (h : c \u2260 0)\n  : Surjective (fun x \u21a6 c * x) :=\nby\n  intro x\n  -- x : \u211d\n  -- \u22a2 \u2203 a, (fun x => c * x) a = x\n  use (x \/ c)\n  -- \u22a2 (fun x => c * x) (x \/ c) = x\n  exact mul_div_cancel' x h\n\n-- 3\u00aa demostraci\u00f3n\nexample\n  (h : c \u2260 0)\n  : Surjective (fun x \u21a6 c * x) :=\nfun x \u21a6 \u27e8x \/ c, mul_div_cancel' x h\u27e9\n\n-- 4\u00aa demostraci\u00f3n\nexample\n  (h : c \u2260 0)\n  : Surjective (fun x \u21a6 c * x) :=\nmul_left_surjective\u2080 h\n\n-- Lemas usados\n-- ============\n\n-- variable (a b : \u211d)\n-- #check (div_mul_cancel a : b \u2260 0 \u2192 (a \/ b) * b = a)\n-- #check (mul_comm a b : a * b = b * a)\n-- #check (mul_div_cancel' a : b \u2260 0 \u2192 b * (a \/ b) = a)\n-- #check (mul_left_surjective\u2080 : c \u2260 0 \u2192 Surjective (fun x \u21a6 c * x))\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