En ℝ, -x ≤ |x|
Demostrar con Lean4 que en \(ℝ\), \(-x ≤ |x|\).
Para ello, completar la siguiente teoría de Lean4:
|
1 2 3 4 5 |
import Mathlib.Data.Real.Basic variable {x : ℝ} example : -x ≤ |x| := by sorry |
Demostración en lenguaje natural
Se usarán los siguientes lemas
\begin{align}
&(∀ x ∈ ℝ)[0 ≤ x → -x ≤ x] \tag{L1} \\
&(∀ x ∈ ℝ)[0 ≤ x → |x| = x] \tag{L2} \\
&(∀ x ∈ ℝ)[x ≤ x] \tag{L3} \\
&(∀ x ∈ ℝ)[x < 0 → |x| = -x] \tag{L4}
\end{align}
Se demostrará por casos según \(x ≥ 0\):
Primer caso: Supongamos que \(x ≥ 0\). Entonces,
\begin{align}
-x &≤ x &&\text{[por L1]} \\
&= |x| &&\text{[por L2]}
\end{align}
Segundo caso: Supongamos que \(x < 0\). Entonces,
\begin{align}
-x &≤ -x &&\text{[por L3]} \\
&= |x| &&\text{[por L4]}
\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 |
import Mathlib.Data.Real.Basic variable {x : ℝ} -- 1ª demostración -- =============== example : -x ≤ |x| := by cases' (le_or_gt 0 x) with h1 h2 . -- h1 : 0 ≤ x show -x ≤ |x| calc -x ≤ x := by exact neg_le_self h1 _ = |x| := (abs_of_nonneg h1).symm . -- h2 : 0 > x show -x ≤ |x| calc -x ≤ -x := by exact le_refl (-x) _ = |x| := (abs_of_neg h2).symm -- 2ª demostración -- =============== example : -x ≤ |x| := by cases' (le_or_gt 0 x) with h1 h2 . -- h1 : 0 ≤ x rw [abs_of_nonneg h1] -- ⊢ -x ≤ x exact neg_le_self h1 . -- h2 : 0 > x rw [abs_of_neg h2] -- 3ª demostración -- =============== example : -x ≤ |x| := by rcases (le_or_gt 0 x) with h1 | h2 . -- h1 : 0 ≤ x rw [abs_of_nonneg h1] -- ⊢ -x ≤ x linarith . -- h2 : 0 > x rw [abs_of_neg h2] -- 4ª demostración -- =============== example : -x ≤ |x| := neg_le_abs_self x -- Lemas usados -- ============ -- variable (y : ℝ) -- #check (abs_of_neg : x < 0 → |x| = -x) -- #check (abs_of_nonneg : 0 ≤ x → |x| = x) -- #check (le_or_gt x y : x ≤ y ∨ x > y) -- #check (le_refl x : x ≤ x) -- #check (neg_le_abs_self x : -x ≤ |x|) -- #check (neg_le_self : 0 ≤ 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.
