En ℝ, x² + y² = 0 ↔ x = 0 ∧ y = 0
Demostrar con Lean4 que si \(x, y ∈ ℝ\), entonces
\[ x^2 + y^2 = 0 ↔ x = 0 ∧ y = 0 \]
Para ello, completar la siguiente teoría de Lean4:
|
1 2 3 4 5 |
import Mathlib.Data.Real.Basic variable {x y : ℝ} example : x^2 + y^2 = 0 ↔ x = 0 ∧ y = 0 := by sorry |
Demostración en lenguaje natural
En la demostración usaremos el siguiente lema auxiliar
\[ (∀ x, y ∈ ℝ)[x² + y² = 0 → x = 0] \]
Para la primera implicación, supongamos que
\[ x² + y² = 0 \tag{1} \]
Entonces, por el lema auxiliar,
\[ x = 0 \tag{2} \]
Además, aplicando la conmutativa a (1), se tiene
\[ y² + x² = 0 \]
y, por el lema auxiliar,
\[ y = 0 \tag{3} \]
De (2) y (3) se tiene
\[ x = 0 ∧ y = 0 \]
Para la segunda implicación, supongamos que
\[ x = 0 ∧ y = 0 \]
Por tanto,
\begin{align}
x² + y² &= 0² + 0² \\
&= 0
\end{align}
En la demostración del lema auxiliar se usarán los siguientes lemas
\begin{align}
&(∀ x ∈ ℝ)(∀ n ∈ ℕ)[x^n = 0 → x = 0] \tag{L1} \\
&(∀ x, y ∈ ℝ)[x ≤ y → y ≤ x → x = y] \tag{L2} \\
&(∀ x, y ∈ ℝ)[0 ≤ y → x ≤ x + y] \tag{L3} \\
&(∀ x ∈ ℝ)[0 ≤ x²] \tag{L4}
\end{align}
Por el lema L1, para demostrar el lema auxiliar basta demostrar
\[ x² = 0 \tag{1} \]
y, por el lema L2, basta demostrar las siguientes desigualdades
\begin{align}
&x² ≤ 0 \tag{2} \\
&0 ≤ x² \tag{3}
\end{align}
La prueba de la (2) es
\begin{align}
x² &≤ x² + y² &&\text{[por L3 y L4]} \\
&= 0 &&\text{[por la hipótesis]}
\end{align}
La (3) se tiene por el lema L4.
Demostraciones con Lean4
|
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 |
import Mathlib.Data.Real.Basic variable {x y : ℝ} -- 1ª demostración del lema auxiliar -- ================================= example (h : x^2 + y^2 = 0) : x = 0 := by have h' : x^2 = 0 := by { apply le_antisymm . show x ^ 2 ≤ 0 calc x ^ 2 ≤ x^2 + y^2 := by simp [le_add_of_nonneg_right, pow_two_nonneg] _ = 0 := by exact h . show 0 ≤ x ^ 2 apply pow_two_nonneg } show x = 0 exact pow_eq_zero h' -- 2ª demostración lema auxiliar -- ============================= example (h : x^2 + y^2 = 0) : x = 0 := by have h' : x^2 = 0 := by { apply le_antisymm . -- ⊢ x ^ 2 ≤ 0 calc x ^ 2 ≤ x^2 + y^2 := by simp [le_add_of_nonneg_right, pow_two_nonneg] _ = 0 := by exact h . -- ⊢ 0 ≤ x ^ 2 apply pow_two_nonneg } exact pow_eq_zero h' -- 3ª demostración lema auxiliar -- ============================= lemma aux (h : x^2 + y^2 = 0) : x = 0 := have h' : x ^ 2 = 0 := by linarith [pow_two_nonneg x, pow_two_nonneg y] pow_eq_zero h' -- 1ª demostración -- =============== example : x^2 + y^2 = 0 ↔ x = 0 ∧ y = 0 := by constructor . -- ⊢ x ^ 2 + y ^ 2 = 0 → x = 0 ∧ y = 0 intro h -- h : x ^ 2 + y ^ 2 = 0 -- ⊢ x = 0 ∧ y = 0 constructor . -- ⊢ x = 0 exact aux h . -- ⊢ y = 0 rw [add_comm] at h -- h : x ^ 2 + y ^ 2 = 0 exact aux h . -- ⊢ x = 0 ∧ y = 0 → x ^ 2 + y ^ 2 = 0 intro h1 -- h1 : x = 0 ∧ y = 0 -- ⊢ x ^ 2 + y ^ 2 = 0 rcases h1 with ⟨h2, h3⟩ -- h2 : x = 0 -- h3 : y = 0 rw [h2, h3] -- ⊢ 0 ^ 2 + 0 ^ 2 = 0 norm_num -- 2ª demostración -- =============== example : x^2 + y^2 = 0 ↔ x = 0 ∧ y = 0 := by constructor . -- ⊢ x ^ 2 + y ^ 2 = 0 → x = 0 ∧ y = 0 intro h -- h : x ^ 2 + y ^ 2 = 0 -- ⊢ x = 0 ∧ y = 0 constructor . -- ⊢ x = 0 exact aux h . -- ⊢ y = 0 rw [add_comm] at h -- h : x ^ 2 + y ^ 2 = 0 exact aux h . -- ⊢ x = 0 ∧ y = 0 → x ^ 2 + y ^ 2 = 0 rintro ⟨h1, h2⟩ -- h1 : x = 0 -- h2 : y = 0 -- ⊢ x ^ 2 + y ^ 2 = 0 rw [h1, h2] -- ⊢ 0 ^ 2 + 0 ^ 2 = 0 norm_num -- 3ª demostración -- =============== example : x ^ 2 + y ^ 2 = 0 ↔ x = 0 ∧ y = 0 := by constructor · -- ⊢ x ^ 2 + y ^ 2 = 0 → x = 0 ∧ y = 0 intro h -- h : x ^ 2 + y ^ 2 = 0 -- ⊢ x = 0 ∧ y = 0 constructor · -- x = 0 exact aux h . -- ⊢ y = 0 rw [add_comm] at h -- h : y ^ 2 + x ^ 2 = 0 exact aux h . -- ⊢ x = 0 ∧ y = 0 → x ^ 2 + y ^ 2 = 0 rintro ⟨rfl, rfl⟩ -- ⊢ 0 ^ 2 + 0 ^ 2 = 0 norm_num -- Lemas usados -- ============ -- #check (add_comm x y : x + y = y + x) -- #check (le_add_of_nonneg_right : 0 ≤ y → x ≤ x + y) -- #check (le_antisymm : x ≤ y → y ≤ x → x = y) -- #check (pow_eq_zero : ∀ {n : ℕ}, x ^ n = 0 → x = 0) -- #check (pow_two_nonneg x : 0 ≤ x ^ 2) |
Demostraciones interactivas
Se puede interactuar con las demostraciones anteriores en Lean 4 Web.
Referencias
- J. Avigad y P. Massot. Mathematics in Lean, p. 37.
