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