smul_closedBall' — Mathlib

English

Scaling a closed ball by c ≠ 0 yields the corresponding closed ball around c·x with radius ||c||·r.

Русский

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

LaTeX

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

Lean4

theorem smul_closedBall' {c : 𝕜} (hc : c ≠ 0) (x : E) (r : ℝ) : c • closedBall x r = closedBall (c • x) (‖c‖ * r) := by
  simp only [← ball_union_sphere, Set.smul_set_union, _root_.smul_ball hc, smul_sphere' hc]

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