isUltrametricDist_of_isNonarchimedean_nnnorm

English

If IsNonarchimedean (nnnorm) then IsUltrametricDist S'.

Русский

Если nnnorm неархимедова, то S' ультраметрично.

LaTeX

$$$\\mathrm{IsNonarchimedean}(\\mathrm{nnnorm}) \\Rightarrow \\mathrm{IsUltrametricDist}(S')$$$

Lean4

theorem isUltrametricDist_of_isNonarchimedean_nnnorm {S' : Type*} [SeminormedAddGroup S']
    (h : IsNonarchimedean (nnnorm : S' → ℝ≥0)) : IsUltrametricDist S' :=
  isUltrametricDist_of_forall_nnnorm_add_le_max_nnnorm h

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