En ℝ, |a| = |a – b + b|
Demostrar con Lean4 que en \(ℝ\), \(|a| = |a – b + b|\)
Para ello, completar la siguiente teoría de Lean4:
|
1 2 3 4 5 6 |
import Mathlib.Data.Real.Basic variable (a b : ℝ) example : |a| = |a - b + b| := by sorry |
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 |
import Mathlib.Data.Real.Basic variable (a b : ℝ) -- 1ª demostración -- =============== example : |a| = |a - b + b| := by congr -- a = a - b + b ring -- Comentario: La táctica congr sustituye una conclusión de la forma -- A = B por las igualdades de sus subtérminos que no no iguales por -- definición. Por ejemplo, sustituye la conclusión (x * f y = g w * f z) -- por las conclusiones (x = g w) y (y = z). -- 2ª demostración -- =============== example (a b : ℝ) : |a| = |a - b + b| := by { congr ; ring } -- 3ª demostración -- =============== example (a b : ℝ) : |a| = |a - b + b| := by ring_nf |
Se puede interactuar con las demostraciones anteriores en Lean 4 Web.
Referencias
- J. Avigad y P. Massot. Mathematics in Lean, p. 41.
