isUltrametricDist_of_isNonarchimedean_norm

English

If a norm on a seminormed additive group is nonarchimedean, then the induced ultrametric distance on the group holds: dist(x+y, x+z) ≤ max(dist(y,z), dist(x,y)) in additive language, equivalently ‖x+y‖ ≤ max(‖x‖, ‖y‖).

Русский

Если норма на полунормированной аддитивной группе неархимедова, то индуцированная ультраметрическая метрика удовлетворяет: dist(x+y, x+z) ≤ max(dist(y,z), dist(x,y)); эквивалентно ‖x+y‖ ≤ max(‖x‖, ‖y‖).

LaTeX

$$$\\Big(\\forall x,y \\in S',\\ \\|x+y\\| \\le \\max(\\|x\\|, \\|y\\|)\\Big) \\implies \\mathrm{IsUltrametricDist}(S')$$$

Lean4

theorem isUltrametricDist_of_isNonarchimedean_norm {S' : Type*} [SeminormedAddGroup S']
    (h : IsNonarchimedean (norm : S' → ℝ)) : IsUltrametricDist S' :=
  isUltrametricDist_of_forall_norm_add_le_max_norm h

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