isNonarchimedean_nnnorm — Mathlib

English

IsUltrametricDist R iff IsNonarchimedean (nnnorm) on R.

Русский

Ультраметричность пространства эквивалентна неархимедовости nnnorm на R.

LaTeX

$$$\\mathrm{IsUltrametricDist}(R) \\iff \\mathrm{IsNonarchimedean}(\\mathrm{nnnorm})$$$

Lean4

theorem isNonarchimedean_nnnorm {R} [SeminormedAddCommGroup R] [IsUltrametricDist R] :
    IsNonarchimedean (‖·‖₊ : R → ℝ) := by
  intro x y
  convert dist_triangle_max 0 x (x + y) using 1
  · simp
  · congr <;> simp [SeminormedAddGroup.dist_eq]

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