dist_triangle_max — Mathlib

English

Let X be an ultrametric space. For all x, y, z in X, the distance d(x, z) is at most the maximum of d(x, y) and d(y, z).

Русский

Пусть X — ультраметрическое пространство. Для любых x, y, z ∈ X выполняется d(x, z) ≤ max{d(x, y), d(y, z)}.

LaTeX

$$$\operatorname{dist}(x,z) \le \max\bigl(\operatorname{dist}(x,y), \operatorname{dist}(y,z)\bigr)$$$

Lean4

theorem dist_triangle_max : dist x z ≤ max (dist x y) (dist y z) :=
  IsUltrametricDist.dist_triangle_max x y z

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