smul_sphere' — Mathlib

English

Scaling a ball by a nonzero c yields a ball with radius scaled by ||c||.

Русский

Умножение шара на ненулевой c даёт шар радиуса ||c||·r вокруг c·x.

LaTeX

$$$c \cdot \mathrm{ball}(x,r) = \mathrm{ball}(c\cdot x, \lVert c \rVert \cdot r).$$$

Lean4

theorem smul_sphere' {c : 𝕜} (hc : c ≠ 0) (x : E) (r : ℝ) : c • sphere x r = sphere (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 only [mem_sphere, dist_smul₀, norm_inv, ← div_eq_inv_mul, div_eq_iff (norm_pos_iff.2 hc).ne', mul_comm r]

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