isNonarchimedean_norm — Mathlib

English

If a norm on a seminormed additive group satisfies the ultrametric inequality for the norm of sums, then the norm is nonarchimedean: ‖x+y‖ ≤ max(‖x‖, ‖y‖) for all x,y.

Русский

Если на полугруппе с нормой выполняется неархимедова неравенство для нормы суммы, то норма неархаримедова: ‖x+y‖ ≤ max(‖x‖, ‖y‖) для всех x,y.

LaTeX

$$$\\forall x,y,\\ \\|x+y\\| \\le \\max(\\|x\\|, \\|y\\|) \\quad\\Rightarrow\\quad \\mathrm{IsNonarchimedean}(\\|\\cdot\\|)$$$

Lean4

theorem isNonarchimedean_norm {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]

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