smul_unitClosedBall — Mathlib

English

For any c in the field, c • closedBall(0,1) equals closedBall(0, ||c||).

Русский

Умножение на шар единицы приводит к замкнутому шару с центром в нуле радиуса ||c||: c • B̄(0,1) = B̄(0,||c||).

LaTeX

$$$c \\cdot \\overline{B}(0, 1) = \\overline{B}(0, \\|c\\|)$$$

Lean4

theorem smul_unitClosedBall (c : 𝕜) : c • closedBall (0 : E) (1 : ℝ) = closedBall (0 : E) ‖c‖ := by
  rw [_root_.smul_closedBall _ _ zero_le_one, smul_zero, mul_one]

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