En ℝ, |x + y| ≤ |x| + |y|
Demostrar con Lean4 que en \(ℝ\),
\[ |x + y| ≤ |x| + |y| \]
Para ello, completar la siguiente teoría de Lean4:
|
1 2 3 4 5 |
import Mathlib.Data.Real.Basic variable {x y : ℝ} example : |x + y| ≤ |x| + |y| := by sorry |
Demostración en lenguaje natural
Se usarán los siguientes lemas
\begin{align}
&(∀ x ∈ ℝ)[0 ≤ x → |x| = x] \tag{L1} \\
&(∀ a, b, c, d ∈ ℝ)[a ≤ b ∧ c ≤ d → a + c ≤ b + d] \tag{L2} \\
&(∀ x ∈ ℝ)[x ≤ |x|] \tag{L3} \\
&(∀ x ∈ ℝ)[x < 0 → |x| = -x] \tag{L4} \\
&(∀ x, y ∈ ℝ)[-(x + y) = -x + -y] \tag{L5} \\
&(∀ x ∈ ℝ)[-x ≤ |x|] \tag{L6}
\end{align}
Se demostrará por casos según \(x + y ≥ 0\):
Primer caso: Supongamos que \(x + y ≥ 0\). Entonces,
\begin{align}
|x + y| &= x + y &&\text{[por L1]} \\
&≤ |x| + |y| &&\text{[por L2 y L3]}
\end{align}
Segundo caso: Supongamos que \(x + y < 0\). Entonces,
\begin{align}
|x + y| &= -(x + y) &&\text{[por L4]} \\
&= -x + -y &&\text{[por L5]} \\
&≤ |x| + |y| &&\text{[por L2 y L6]}
\end{align}
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 |
import Mathlib.Data.Real.Basic variable {x y : ℝ} -- 1ª demostración -- =============== example : |x + y| ≤ |x| + |y| := by rcases le_or_gt 0 (x + y) with h1 | h2 · -- h1 : 0 ≤ x + y show |x + y| ≤ |x| + |y| calc |x + y| = x + y := by exact abs_of_nonneg h1 _ ≤ |x| + |y| := add_le_add (le_abs_self x) (le_abs_self y) . -- h2 : 0 > x + y show |x + y| ≤ |x| + |y| calc |x + y| = -(x + y) := by exact abs_of_neg h2 _ = -x + -y := by exact neg_add x y _ ≤ |x| + |y| := add_le_add (neg_le_abs_self x) (neg_le_abs_self y) -- 2ª demostración -- =============== example : |x + y| ≤ |x| + |y| := by rcases le_or_gt 0 (x + y) with h1 | h2 · -- h1 : 0 ≤ x + y rw [abs_of_nonneg h1] -- ⊢ x + y ≤ |x| + |y| exact add_le_add (le_abs_self x) (le_abs_self y) . -- h2 : 0 > x + y rw [abs_of_neg h2] -- ⊢ -(x + y) ≤ |x| + |y| calc -(x + y) = -x + -y := by exact neg_add x y _ ≤ |x| + |y| := add_le_add (neg_le_abs_self x) (neg_le_abs_self y) -- 2ª demostración -- =============== example : |x + y| ≤ |x| + |y| := by rcases le_or_gt 0 (x + y) with h1 | h2 · -- h1 : 0 ≤ x + y rw [abs_of_nonneg h1] -- ⊢ x + y ≤ |x| + |y| linarith [le_abs_self x, le_abs_self y] . -- h2 : 0 > x + y rw [abs_of_neg h2] -- ⊢ -(x + y) ≤ |x| + |y| linarith [neg_le_abs_self x, neg_le_abs_self y] -- 3ª demostración -- =============== example : |x + y| ≤ |x| + |y| := abs_add x y -- Lemas usados -- ============ -- variable (a b c d : ℝ) -- #check (abs_add x y : |x + y| ≤ |x| + |y|) -- #check (abs_of_neg : x < 0 → |x| = -x) -- #check (abs_of_nonneg : 0 ≤ x → |x| = x) -- #check (add_le_add : a ≤ b → c ≤ d → a + c ≤ b + d) -- #check (le_abs_self a : a ≤ |a|) -- #check (le_or_gt x y : x ≤ y ∨ x > y) -- #check (neg_add x y : -(x + y) = -x + -y) -- #check (neg_le_abs_self x : -x ≤ |x|) |
Demostraciones interactivas
Se puede interactuar con las demostraciones anteriores en Lean 4 Web.
Referencias
- J. Avigad y P. Massot. Mathematics in Lean, p. 38.
En 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 38 39 40 41 |
theory Desigualdad_triangular_para_valor_absoluto imports Main HOL.Real begin (* 1ª demostración *) lemma fixes x y :: real shows "¦x + y¦ ≤ ¦x¦ + ¦y¦" proof - { assume h1: "0 ≤ x + y" then have "¦x + y¦ = x + y" by simp also have "... ≤ ¦x¦ + ¦y¦" by simp finally have "¦x + y¦ ≤ ¦x¦ + ¦y¦" . } moreover { assume h2: "0 > x + y" then have "¦x + y¦ = -(x + y)" by simp also have "... = -x + -y" by simp also have "... ≤ ¦x¦ + ¦y¦" by simp finally have "¦x + y¦ ≤ ¦x¦ + ¦y¦" . } ultimately show ?thesis by simp qed (* 2ª demostración *) lemma fixes x y :: real shows "¦x + y¦ ≤ ¦x¦ + ¦y¦" by (rule abs_triangle_ineq) (* 3ª demostración *) lemma fixes x y :: real shows "¦x + y¦ ≤ ¦x¦ + ¦y¦" by simp end |
