Si |x + 3| < 5, entonces -8 < x < 2
Demostrar con Lean4 que si \(|x + 3| < 5\), entonces \(-8 < x < 2\).
Para ello, completar la siguiente teoría de Lean4:
|
1 2 3 4 5 6 |
import Mathlib.Data.Real.Basic variable (x y : ℝ) example : |x + 3| < 5 → -8 < x ∧ x < 2 := by sorry |
Demostración en lenguaje natural
Supongamos que
\[ |x + 3| < 5 \]
entonces
\[ -5 < x + 3 < 5 \]
por tanto
\[ -8 < x < 2 \]
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 |
import Mathlib.Data.Real.Basic variable (x y : ℝ) -- 1ª demostración -- =============== example : |x + 3| < 5 → -8 < x ∧ x < 2 := by rw [abs_lt] -- ⊢ -5 < x + 3 ∧ x + 3 < 5 → -8 < x ∧ x < 2 intro h -- h : -5 < x + 3 ∧ x + 3 < 5 -- ⊢ -8 < x ∧ x < 2 constructor . -- ⊢ -8 < x linarith . -- x < 2 linarith -- 2ª demostración -- =============== example : |x + 3| < 5 → -8 < x ∧ x < 2 := by rw [abs_lt] intro h constructor <;> linarith -- Comentario: La composición (constructor <;> linarith) aplica constructor y a -- continuación le aplica linarith a cada subojetivo. -- 3ª demostración -- =============== example : |x + 3| < 5 → -8 < x ∧ x < 2 := by rw [abs_lt] exact fun _ ↦ ⟨by linarith, by linarith⟩ -- Lemas usados -- ============ -- #check (abs_lt: |x| < y ↔ -y < x ∧ 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. 37.
