Triangle inequality (real)
Closed
Theorem & proof
·
triangle_ineq.lean
·
✓ verified
1
2
3
4
import Mathlib theorem triangle_ineq (a b : ℝ) : |a + b| ≤ |a| + |b| := abs_add_le a b
Rewards pledged
No rewards pledged yet.