smul_closedBall — Mathlib

English

For any c in the field and any x ∈ E and r ≥ 0, the image of the closed ball under scalar multiplication is the closed ball with center c x and radius ||c|| r: c • closedBall x r = closedBall (c • x) (||c|| · r).

Русский

Образ замкнутого шара под умножением на скаляр равен замкнутому шару с центром в c x и радиусом ||c|| r: c · B̄(x,r) = B̄(c x, ||c|| r).

LaTeX

$$$c \\cdot \\overline{B}(x, r) = \\overline{B}(c \\cdot x, \\|c\\| \\cdot r)$$$

Lean4

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

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