dist_triangle — Mathlib

English

The distance satisfies the triangle inequality: dist(x,z) ≤ dist(x,y) + dist(y,z).

Русский

Расстояние удовлетворяет неравенству треугольника: dist(x,z) ≤ dist(x,y) + dist(y,z).

LaTeX

$$$$ \operatorname{dist}(x,z) \le \operatorname{dist}(x,y) + \operatorname{dist}(y,z) $$$$

Lean4

protected theorem dist_triangle (x y z : ∀ n, E n) : dist x z ≤ dist x y + dist y z :=
  calc
    dist x z ≤ max (dist x y) (dist y z) := dist_triangle_nonarch x y z
    _ ≤ dist x y + dist y z := max_le_add_of_nonneg (PiNat.dist_nonneg _ _) (PiNat.dist_nonneg _ _)

Похожие утверждения