instIsUltrametricDist — Mathlib

English

PadicAlgCl p is ultrametric: the distance function d satisfies the strong triangle inequality d(x,z) ≤ max(d(x,y), d(y,z)).

Русский

PadicAlgCl p является ультраметрическим пространством: расстояние удовлетворяет неравенству сильной треугольности.

LaTeX

$$$$d(x,z) \le \max\{d(x,y), d(y,z)\}\quad\text{for all } x,y,z \in \operatorname{PadicAlgCl}(p).$$$$

Lean4

instance : IsUltrametricDist (PadicAlgCl p) :=
  IsUltrametricDist.isUltrametricDist_of_forall_norm_add_le_max_norm (PadicAlgCl.isNonarchimedean p)

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