English
Let α be a seminormed ring, β a normed module over α. For any s ∈ α and x,y ∈ β, the distance after scaling by s scales by the norm of s: dist(s • x, s • y) = ||s|| · dist(x,y).
Русский
Пусть α — полунормируемое кольцо, β — нормируемый модуль над α. Для всех s ∈ α и x,y ∈ β расстояние после умножения на s масштабируется пропорционально норме s: dist(s • x, s • y) = ||s|| · dist(x,y).
LaTeX
$$$$\\operatorname{dist}(s \\cdot x, s \\cdot y) = \\|s\\| \\, \\operatorname{dist}(x,y).$$$$
Lean4
theorem dist_smul₀ (s : α) (x y : β) : dist (s • x) (s • y) = ‖s‖ * dist x y := by
simp_rw [dist_eq_norm, (norm_smul s (x - y)).symm, smul_sub]
