infDist_smul₀ — Mathlib

English

For nonzero c, the infimum distance between c·x and c·s equals |c| times the infEdist between x and s.

Русский

Если c ≠ 0, инфиминальное евклидово расстояние между c·x и c·s равно |c| умножить на infEdist(x,s).

LaTeX

$$$\operatorname{infEdist}(c\cdot x, c\cdot s) = \|c\|_+ \cdot \operatorname{infEdist}(x,s).$$$

Lean4

theorem infDist_smul₀ {c : 𝕜} (hc : c ≠ 0) (s : Set E) (x : E) :
    Metric.infDist (c • x) (c • s) = ‖c‖ * Metric.infDist x s := by
  simp_rw [Metric.infDist, infEdist_smul₀ hc s, ENNReal.toReal_smul, NNReal.smul_def, coe_nnnorm, smul_eq_mul]

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