edist_smul₀ — Mathlib

English

The extended distance (edist) scales under scalar multiplication by the nonnegative norm: edist(s • x, s • y) = ||s||₊ · edist(x,y).

Русский

Расстояние в расширенной шкале масштабируется: edist(s • x, s • y) = ||s||₊ · edist(x,y).

LaTeX

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

Lean4

theorem edist_smul₀ (s : α) (x y : β) : edist (s • x) (s • y) = ‖s‖₊ • edist x y := by
  simp only [edist_nndist, nndist_smul₀, ENNReal.coe_mul, ENNReal.smul_def, smul_eq_mul]

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