smul_sphere — Mathlib

English

For a nontrivial normed space E, a scalar c maps the sphere S(x,r) to the sphere S(cx, ||c|| r): c • S(x,r) = S(cx, ||c|| r).

Русский

Для ненулевого пространства E скаляр c отображает сферу S(x,r) в сферу S(cx, ||c|| r).

LaTeX

$$$c \\cdot \\mathbb{S}(x, r) = \\mathbb{S}(c \\cdot x, \\|c\\| \\cdot r)$$$

Lean4

theorem smul_sphere [Nontrivial E] (c : 𝕜) (x : E) {r : ℝ} (hr : 0 ≤ r) : c • sphere x r = sphere (c • x) (‖c‖ * r) :=
  by
  rcases eq_or_ne c 0 with (rfl | hc)
  · simp [zero_smul_set, Set.singleton_zero, hr]
  · exact smul_sphere' hc x r

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