isUltrametricDist_iff_isNonarchimedean_norm

English

In a normed additive group (or more generally a seminormed group), ultrametric distance is equivalent to the norm being nonarchimedean.

Русский

В нормированной аддитивной группе ультраметричность расстояния равносильна тому, что норма неархимедова.

LaTeX

$$$\\mathrm{IsUltrametricDist}(R) \\iff \\mathrm{IsNonarchimedean}(\\|\\cdot\\|)$$$

Lean4

theorem isUltrametricDist_iff_isNonarchimedean_norm {R} [SeminormedAddCommGroup R] :
    IsUltrametricDist R ↔ IsNonarchimedean (‖·‖ : R → ℝ) :=
  ⟨fun h => h.isNonarchimedean_norm, IsUltrametricDist.isUltrametricDist_of_isNonarchimedean_norm⟩

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