smul_unitBall

Mathlib.Analysis.Normed.Module.Ball.Pointwise

URI: https://scilib.ai/kg/mathlib#smul_unitBall

English

For c ≠ 0, c · sphere(x,r) = sphere(c·x, ||c|| · r).

Русский

При c ≠ 0 выполняется c · sphere(x,r) = sphere(c·x, ||c|| · r).

LaTeX

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

Lean4

theorem smul_unitBall {c : 𝕜} (hc : c ≠ 0) : c • ball (0 : E) (1 : ℝ) = ball (0 : E) ‖c‖ := by
  rw [_root_.smul_ball hc, smul_zero, mul_one]

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru