Reverse_Triangle_Inequality_Metric
Provedinequalitiesmetric-spacesproofwikitriangle-inequality
Let M = (X, d) be a metric space. Then for all x, y, z in X: |d(x,z) - d(y,z)| <= d(x,y).
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem Reverse_Triangle_Inequality_Metric {X : Type _} [PseudoMetricSpace X] (x y z : X) : |dist x z - dist y z| <= dist x y := by sorrySource