ball_one_mul_singleton

Mathlib.Analysis.Normed.Group.Pointwise

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

English

The ball around 1, δ multiplied by a singleton equals the ball around x: ball(1, δ) * {x} = ball(x, δ).

Русский

Шар вокруг 1, δ, умноженный на единичный элемент, равен шарa вокруг x: ball(1, δ) * {x} = ball(x, δ).

LaTeX

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

Lean4

@[to_additive]
theorem ball_one_mul_singleton : ball 1 δ * { x } = ball x δ := by simp

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

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

Разделы

Аффилиация

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