En ℝ, si x < |y|, entonces x < y ó x < -y
Demostrar con Lean4 que en \(ℝ\), si \(x < |y|\), entonces \(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 ∨ x < -y := by sorry |
Demostración en lenguaje natural
Se demostrará por casos según \(y ≥ 0\).
Primer caso: Supongamos que \(y ≥ 0\). Entonces, \(|y| = y\) y, por tanto, \(x < y\).
Segundo caso: Supongamos que \(y < 0\). Entonces, \(|y| = -y\) y, por tanto, \(x < -y\).
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 |
import Mathlib.Data.Real.Basic variable {x y : ℝ} -- 1ª demostración -- =============== example : x < |y| → x < y ∨ x < -y := by intro h1 -- h1 : x < |y| -- ⊢ x < y ∨ x < -y cases' le_or_gt 0 y with h2 h3 . -- h2 : 0 ≤ y left -- ⊢ x < y rwa [abs_of_nonneg h2] at h1 . -- h3 : 0 > y right -- ⊢ x < -y rwa [abs_of_neg h3] at h1 -- 2ª demostración -- =============== example : x < |y| → x < y ∨ x < -y := lt_abs.mp -- Lemas usados -- ============ -- #check (le_or_gt x y : x ≤ y ∨ x > y) -- #check (abs_of_nonneg : 0 ≤ x → abs x = x) -- #check (abs_of_neg : x < 0 → abs x = -x) -- #check (lt_abs : x < |y| ↔ x < y ∨ x < -y) |
Demostraciones interactivas
Se puede interactuar con las demostraciones anteriores en Lean 4 Web.
Referencias
- J. Avigad y P. Massot. Mathematics in Lean, p. 38.
