dist_triangle — Mathlib

English

For all x,y,z in the completion, dist x z ≤ dist x y + dist y z.

Русский

Для любых x,y,z в завершении выполняется неравенство треугольника: dist(x,z) ≤ dist(x,y) + dist(y,z).

LaTeX

$$$\operatorname{dist} x z \leq \operatorname{dist} x y + \operatorname{dist} y z$$$

Lean4

protected theorem dist_triangle (x y z : Completion α) : dist x z ≤ dist x y + dist y z :=
  by
  refine induction_on₃ x y z ?_ ?_
  ·
    refine isClosed_le ?_ (Continuous.add ?_ ?_) <;>
      apply_rules [Completion.continuous_dist, Continuous.fst, Continuous.snd, continuous_id]
  · intro a b c
    rw [Completion.dist_eq, Completion.dist_eq, Completion.dist_eq]
    exact dist_triangle a b c

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