isUltrametricDist_iff_isNonarchimedean_nnnorm

English

IsUltrametricDist R iff IsNonarchimedean (norm) on R.

Русский

Ультраметричность равносильна неархимедовой норме на R.

LaTeX

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

Lean4

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

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