Si (∃ x, y ∈ ℝ)[z = x² + y² ∨ z = x² + y² + 1], entonces z ≥ 0
Demostrar con Lean4 que si \((∃ x, y ∈ ℝ)[z = x² + y² ∨ z = x² + y² + 1]\), entonces \(z ≥ 0\).
Para ello, completar la siguiente teoría de Lean4:
|
1 2 3 4 5 6 7 8 |
import Mathlib.Data.Real.Basic import Mathlib.Tactic variable {z : ℝ} example (h : ∃ x y, z = x^2 + y^2 ∨ z = x^2 + y^2 + 1) : z ≥ 0 := by sorry |
Demostración en lenguaje natural
Usaremos los siguientes lemas
\begin{align}
&(∀ x ∈ ℝ)[x² ≥ 0] \tag{L1} \\
&(∀ x, y ∈ ℝ)[x ≥ 0 → y ≥ 0 → x + y ≥ 0] \tag{L2} \\
&1 ≥ 0 \tag{L3}
\end{align}
Sean \(a\) y \(b\) tales que
\[ z = a² + b² ∨ z = a² + b² + 1 \]
Entonces, por L1, se tiene que
\begin{align}
&a² ≥ 0 \tag{1} \\
&b² ≥ 0 \tag{2}
\end{align}
En el primer caso, \(z = a² + b²\) y se tiene que \(z ≥ 0\) por el lema L2 aplicado a (1) y (2).
En el segundo caso, \(z = a² + b² + 1\) y se tiene que \(z ≥ 0\) por el lema L2 aplicado a (1), (2) y L3.
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 131 |
import Mathlib.Data.Real.Basic import Mathlib.Tactic variable {z : ℝ} -- 1ª demostración -- =============== example (h : ∃ x y, z = x^2 + y^2 ∨ z = x^2 + y^2 + 1) : z ≥ 0 := by rcases h with ⟨a, b, h1⟩ -- a b : ℝ -- h1 : z = a ^ 2 + b ^ 2 ∨ z = a ^ 2 + b ^ 2 + 1 have h2 : a ^ 2 ≥ 0 := pow_two_nonneg a have h3 : b ^ 2 ≥ 0 := pow_two_nonneg b have h4 : a ^ 2 + b ^ 2 ≥ 0 := add_nonneg h2 h3 rcases h1 with h5 | h6 . -- h5 : z = a ^ 2 + b ^ 2 show z ≥ 0 calc z = a ^ 2 + b ^ 2 := h5 _ ≥ 0 := add_nonneg h2 h3 . -- h6 : z = a ^ 2 + b ^ 2 + 1 show z ≥ 0 calc z = (a ^ 2 + b ^ 2) + 1 := h6 _ ≥ 0 := add_nonneg h4 zero_le_one -- 2ª demostración -- =============== example (h : ∃ x y, z = x^2 + y^2 ∨ z = x^2 + y^2 + 1) : z ≥ 0 := by rcases h with ⟨a, b, h1 | h2⟩ . -- h1 : z = a ^ 2 + b ^ 2 have h1a : a ^ 2 ≥ 0 := pow_two_nonneg a have h1b : b ^ 2 ≥ 0 := pow_two_nonneg b show z ≥ 0 calc z = a ^ 2 + b ^ 2 := h1 _ ≥ 0 := add_nonneg h1a h1b . -- h2 : z = a ^ 2 + b ^ 2 + 1 have h2a : a ^ 2 ≥ 0 := pow_two_nonneg a have h2b : b ^ 2 ≥ 0 := pow_two_nonneg b have h2c : a ^ 2 + b ^ 2 ≥ 0 := add_nonneg h2a h2b show z ≥ 0 calc z = (a ^ 2 + b ^ 2) + 1 := h2 _ ≥ 0 := add_nonneg h2c zero_le_one -- 3ª demostración -- =============== example (h : ∃ x y, z = x^2 + y^2 ∨ z = x^2 + y^2 + 1) : z ≥ 0 := by rcases h with ⟨a, b, h1 | h2⟩ . -- h1 : z = a ^ 2 + b ^ 2 rw [h1] -- ⊢ a ^ 2 + b ^ 2 ≥ 0 apply add_nonneg . -- ⊢ 0 ≤ a ^ 2 apply pow_two_nonneg . -- ⊢ 0 ≤ b ^ 2 apply pow_two_nonneg . -- h2 : z = a ^ 2 + b ^ 2 + 1 rw [h2] -- ⊢ a ^ 2 + b ^ 2 + 1 ≥ 0 apply add_nonneg . -- ⊢ 0 ≤ a ^ 2 + b ^ 2 apply add_nonneg . -- ⊢ 0 ≤ a ^ 2 apply pow_two_nonneg . -- ⊢ 0 ≤ b ^ 2 apply pow_two_nonneg . -- ⊢ 0 ≤ 1 exact zero_le_one -- 4ª demostración -- =============== example (h : ∃ x y, z = x^2 + y^2 ∨ z = x^2 + y^2 + 1) : z ≥ 0 := by rcases h with ⟨a, b, rfl | rfl⟩ . -- ⊢ a ^ 2 + b ^ 2 ≥ 0 apply add_nonneg . -- ⊢ 0 ≤ a ^ 2 apply pow_two_nonneg . -- ⊢ 0 ≤ b ^ 2 apply pow_two_nonneg . -- ⊢ a ^ 2 + b ^ 2 + 1 ≥ 0 apply add_nonneg . -- ⊢ 0 ≤ a ^ 2 + b ^ 2 apply add_nonneg . -- ⊢ 0 ≤ a ^ 2 apply pow_two_nonneg . -- ⊢ 0 ≤ b ^ 2 apply pow_two_nonneg . -- ⊢ 0 ≤ 1 exact zero_le_one -- 5ª demostración -- =============== example (h : ∃ x y, z = x^2 + y^2 ∨ z = x^2 + y^2 + 1) : z ≥ 0 := by rcases h with ⟨a, b, rfl | rfl⟩ . -- ⊢ a ^ 2 + b ^ 2 ≥ 0 nlinarith . -- ⊢ a ^ 2 + b ^ 2 + 1 ≥ 0 nlinarith -- 6ª demostración -- =============== example (h : ∃ x y, z = x^2 + y^2 ∨ z = x^2 + y^2 + 1) : z ≥ 0 := by rcases h with ⟨a, b, rfl | rfl⟩ <;> nlinarith -- Lemas usados -- ============ -- variable (x y : ℝ) -- #check (add_nonneg : 0 ≤ x → 0 ≤ y → 0 ≤ x + y) -- #check (pow_two_nonneg x : 0 ≤ x ^ 2) -- #check (zero_le_one : 0 ≤ 1) |
Demostraciones interactivas
Se puede interactuar con las demostraciones anteriores en Lean 4 Web.
Referencias
- J. Avigad y P. Massot. Mathematics in Lean, p. 39.
Demostraciones con Isabelle/HOL
|
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 |
theory Desigualdad_con_rcases imports Main "HOL.Real" begin (* 1ª demostración *) lemma assumes "∃x y :: real. (z = x^2 + y^2 ∨ z = x^2 + y^2 + 1)" shows "z ≥ 0" proof - obtain x y where hxy: "z = x^2 + y^2 ∨ z = x^2 + y^2 + 1" using assms by auto { assume "z = x^2 + y^2" have "x^2 + y^2 ≥ 0" by simp then have "z ≥ 0" using `z = x^2 + y^2` by simp } { assume "z = x^2 + y^2 + 1" have "x^2 + y^2 ≥ 0" by simp then have "z ≥ 1" using `z = x^2 + y^2 + 1` by simp } with hxy show "z ≥ 0" by auto qed (* 2ª demostración *) lemma assumes "∃x y :: real. (z = x^2 + y^2 ∨ z = x^2 + y^2 + 1)" shows "z ≥ 0" proof - obtain x y where hxy: "z = x^2 + y^2 ∨ z = x^2 + y^2 + 1" using assms by auto with hxy show "z ≥ 0" by auto qed (* 3ª demostración *) lemma assumes "∃x y :: real. (z = x^2 + y^2 ∨ z = x^2 + y^2 + 1)" shows "z ≥ 0" using assms by fastforce end |
