Demostrar con Lean4 que si \(x, y \u2208 \u211d\), entonces
\n\[ x^2 + y^2 = 0 \u2194 x = 0 \u2227 y = 0 \]<\/p>\n
Para ello, completar la siguiente teor\u00eda de Lean4:<\/p>\n
\nimport Mathlib.Data.Real.Basic\nvariable {x y : \u211d}\n\nexample : x^2 + y^2 = 0 \u2194 x = 0 \u2227 y = 0 :=\nby sorry\n<\/pre>\n<\/p>\n
Demostraci\u00f3n en lenguaje natural<\/b><\/p>\n
En la demostraci\u00f3n usaremos el siguiente lema auxiliar
\n\[ (\u2200 x, y \u2208 \u211d)[x\u00b2 + y\u00b2 = 0 \u2192 x = 0] \]<\/p>\n
Para la primera implicaci\u00f3n, supongamos que
\n\[ x\u00b2 + y\u00b2 = 0 \tag{1} \]
\nEntonces, por el lema auxiliar,
\n\[ x = 0 \tag{2} \]
\nAdem\u00e1s, aplicando la conmutativa a (1), se tiene
\n\[ y\u00b2 + x\u00b2 = 0 \]
\ny, por el lema auxiliar,
\n\[ y = 0 \tag{3} \]
\nDe (2) y (3) se tiene
\n\[ x = 0 \u2227 y = 0 \]<\/p>\n
Para la segunda implicaci\u00f3n, supongamos que
\n\[ x = 0 \u2227 y = 0 \]
\nPor tanto,
\n\begin{align}
\n x\u00b2 + y\u00b2 &= 0\u00b2 + 0\u00b2 \\
\n &= 0
\n\end{align}<\/p>\n
En la demostraci\u00f3n del lema auxiliar se usar\u00e1n los siguientes lemas
\n\begin{align}
\n &(\u2200 x \u2208 \u211d)(\u2200 n \u2208 \u2115)[x^n = 0 \u2192 x = 0] \tag{L1} \\
\n &(\u2200 x, y \u2208 \u211d)[x \u2264 y \u2192 y \u2264 x \u2192 x = y] \tag{L2} \\
\n &(\u2200 x, y \u2208 \u211d)[0 \u2264 y \u2192 x \u2264 x + y] \tag{L3} \\
\n &(\u2200 x \u2208 \u211d)[0 \u2264 x\u00b2] \tag{L4}
\n\end{align}<\/p>\n
Por el lema L1, para demostrar el lema auxiliar basta demostrar
\n\[ x\u00b2 = 0 \tag{1} \]
\ny, por el lema L2, basta demostrar las siguientes desigualdades
\n\begin{align}
\n &x\u00b2 \u2264 0 \tag{2} \\
\n &0 \u2264 x\u00b2 \tag{3}
\n\end{align}<\/p>\n
La prueba de la (2) es
\n\begin{align}
\n x\u00b2 &\u2264 x\u00b2 + y\u00b2 &&\text{[por L3 y L4]} \\
\n &= 0 &&\text{[por la hip\u00f3tesis]}
\n\end{align}<\/p>\n
La (3) se tiene por el lema L4.<\/p>\n
Demostraciones con Lean4<\/b><\/p>\n\nimport Mathlib.Data.Real.Basic\nvariable {x y : \u211d}\n\n-- 1\u00aa demostraci\u00f3n del lema auxiliar\n-- =================================\n\nexample\n (h : x^2 + y^2 = 0)\n : x = 0 :=\nby\n have h' : x^2 = 0 := by\n { apply le_antisymm\n . show x ^ 2 \u2264 0\n calc x ^ 2 \u2264 x^2 + y^2 := by simp [le_add_of_nonneg_right,\n pow_two_nonneg]\n _ = 0 := by exact h\n . show 0 \u2264 x ^ 2\n apply pow_two_nonneg }\n show x = 0\n exact pow_eq_zero h'\n\n-- 2\u00aa demostraci\u00f3n lema auxiliar\n-- =============================\n\nexample\n (h : x^2 + y^2 = 0)\n : x = 0 :=\nby\n have h' : x^2 = 0 := by\n { apply le_antisymm\n . -- \u22a2 x ^ 2 \u2264 0\n calc x ^ 2 \u2264 x^2 + y^2 := by simp [le_add_of_nonneg_right,\n pow_two_nonneg]\n _ = 0 := by exact h\n . -- \u22a2 0 \u2264 x ^ 2\n apply pow_two_nonneg }\n exact pow_eq_zero h'\n\n-- 3\u00aa demostraci\u00f3n lema auxiliar\n-- =============================\n\nlemma aux\n (h : x^2 + y^2 = 0)\n : x = 0 :=\n have h' : x ^ 2 = 0 := by linarith [pow_two_nonneg x, pow_two_nonneg y]\n pow_eq_zero h'\n\n-- 1\u00aa demostraci\u00f3n\n-- ===============\n\nexample : x^2 + y^2 = 0 \u2194 x = 0 \u2227 y = 0 :=\nby\n constructor\n . -- \u22a2 x ^ 2 + y ^ 2 = 0 \u2192 x = 0 \u2227 y = 0\n intro h\n -- h : x ^ 2 + y ^ 2 = 0\n -- \u22a2 x = 0 \u2227 y = 0\n constructor\n . -- \u22a2 x = 0\n exact aux h\n . -- \u22a2 y = 0\n rw [add_comm] at h\n -- h : x ^ 2 + y ^ 2 = 0\n exact aux h\n . -- \u22a2 x = 0 \u2227 y = 0 \u2192 x ^ 2 + y ^ 2 = 0\n intro h1\n -- h1 : x = 0 \u2227 y = 0\n -- \u22a2 x ^ 2 + y ^ 2 = 0\n rcases h1 with \u27e8h2, h3\u27e9\n -- h2 : x = 0\n -- h3 : y = 0\n rw [h2, h3]\n -- \u22a2 0 ^ 2 + 0 ^ 2 = 0\n norm_num\n\n-- 2\u00aa demostraci\u00f3n\n-- ===============\n\nexample : x^2 + y^2 = 0 \u2194 x = 0 \u2227 y = 0 :=\nby\n constructor\n . -- \u22a2 x ^ 2 + y ^ 2 = 0 \u2192 x = 0 \u2227 y = 0\n intro h\n -- h : x ^ 2 + y ^ 2 = 0\n -- \u22a2 x = 0 \u2227 y = 0\n constructor\n . -- \u22a2 x = 0\n exact aux h\n . -- \u22a2 y = 0\n rw [add_comm] at h\n -- h : x ^ 2 + y ^ 2 = 0\n exact aux h\n . -- \u22a2 x = 0 \u2227 y = 0 \u2192 x ^ 2 + y ^ 2 = 0\n rintro \u27e8h1, h2\u27e9\n -- h1 : x = 0\n -- h2 : y = 0\n -- \u22a2 x ^ 2 + y ^ 2 = 0\n rw [h1, h2]\n -- \u22a2 0 ^ 2 + 0 ^ 2 = 0\n norm_num\n\n-- 3\u00aa demostraci\u00f3n\n-- ===============\n\nexample : x ^ 2 + y ^ 2 = 0 \u2194 x = 0 \u2227 y = 0 := by\n constructor\n \u00b7 -- \u22a2 x ^ 2 + y ^ 2 = 0 \u2192 x = 0 \u2227 y = 0\n intro h\n -- h : x ^ 2 + y ^ 2 = 0\n -- \u22a2 x = 0 \u2227 y = 0\n constructor\n \u00b7 -- x = 0\n exact aux h\n . -- \u22a2 y = 0\n rw [add_comm] at h\n -- h : y ^ 2 + x ^ 2 = 0\n exact aux h\n . -- \u22a2 x = 0 \u2227 y = 0 \u2192 x ^ 2 + y ^ 2 = 0\n rintro \u27e8rfl, rfl\u27e9\n -- \u22a2 0 ^ 2 + 0 ^ 2 = 0\n norm_num\n\n-- Lemas usados\n-- ============\n\n-- #check (add_comm x y : x + y = y + x)\n-- #check (le_add_of_nonneg_right : 0 \u2264 y \u2192 x \u2264 x + y)\n-- #check (le_antisymm : x \u2264 y \u2192 y \u2264 x \u2192 x = y)\n-- #check (pow_eq_zero : \u2200 {n : \u2115}, x ^ n = 0 \u2192 x = 0)\n-- #check (pow_two_nonneg x : 0 \u2264 x ^ 2)\n<\/pre>\nDemostraciones interactivas<\/b><\/p>\n
Se puede interactuar con las demostraciones anteriores en Lean 4 Web<\/a>.<\/p>\nReferencias<\/b><\/p>\n