Distance_on_Real_Numbers_is_Metric_v2
Provedmetric-spaceproofwikireal-numberstopology
The standard distance function on the real numbers satisfies the triangle inequality.
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem Distance_on_Real_Numbers_is_Metric_v2 (x y z : ℝ) : dist x z ≤ dist x y + dist y z := by sorry
Source