nndist_smul₀ — Mathlib

English

In a normed ring acting on a normed module, the nonnegative distance (NN-distance) also scales by the nonnegative norm: nndist(s • x, s • y) = ||s||₊ · nndist(x,y).

Русский

В нормированном кольце, действующем на нормированном модуле, сохраняется неотрицованная дистанция: nndist(s • x, s • y) = ||s||₊ · nndist(x,y).

LaTeX

$$$$\\mathrm{nndist}(s \\cdot x, s \\cdot y) = \\|s\\|_+ \\cdot \\mathrm{nndist}(x,y).$$$$

Lean4

theorem nndist_smul₀ (s : α) (x y : β) : nndist (s • x) (s • y) = ‖s‖₊ * nndist x y :=
  NNReal.eq <| dist_smul₀ s x y

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