smul_ball — Mathlib

English

For c ≠ 0, the distance between c·x and c·s equals ||c|| times the distance between x and s.

Русский

При c ≠ 0 расстояние между c·x и c·s равно ||c|| умножить на расстояние между x и s.

LaTeX

$$$\operatorname{infDist}(c\cdot x, c\cdot s) = \|c\| \cdot \operatorname{infDist}(x,s).$$$

Lean4

theorem smul_ball {c : 𝕜} (hc : c ≠ 0) (x : E) (r : ℝ) : c • ball x r = ball (c • x) (‖c‖ * r) :=
  by
  ext y
  rw [mem_smul_set_iff_inv_smul_mem₀ hc]
  conv_lhs => rw [← inv_smul_smul₀ hc x]
  simp [← div_eq_inv_mul, div_lt_iff₀ (norm_pos_iff.2 hc), mul_comm _ r, dist_smul₀]

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