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 |
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 |