singleton_div_ball_one

Mathlib.Analysis.Normed.Group.Pointwise

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

English

Division by the unit ball maps to the ball around x: {x} / ball(1, δ) = ball(x, δ).

Русский

Деление единичного шара на шар единицы даёт шар вокруг x: {x} / ball(1, δ) = ball(x, δ).

LaTeX

$$$${x} / B(1,\delta) = B(x,\delta)$$$$

Lean4

@[to_additive]
theorem singleton_div_ball_one : { x } / ball 1 δ = ball x δ := by rw [singleton_div_ball, div_one]

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

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

Разделы

Аффилиация

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