dist_smul_le — Mathlib

English

For all s ∈ α, x, y ∈ β, the distance after scaling is controlled by the distance before: dist(s • x, s • y) ≤ ‖s‖ · dist(x,y).

Русский

Для всех s ∈ α, x,y ∈ β расстояние после умножения на скаляр контролируется расстоянием до умножения: dist(s • x, s • y) ≤ ‖s‖ · dist(x,y).

LaTeX

$$$\\operatorname{dist}(s \\cdot x, s \\cdot y) \\le \\|s\\| \\cdot \\operatorname{dist}(x, y)$$$

Lean4

theorem dist_smul_le (s : α) (x y : β) : dist (s • x) (s • y) ≤ ‖s‖ * dist x y := by
  simpa only [dist_eq_norm, sub_zero] using dist_smul_pair s x y

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