ball_mul_one

Mathlib.Analysis.Normed.Group.Pointwise

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

English

Ball(1, δ) multiplied by a set s on the left yields thickening by δ: ball 1 δ * s = thickening(δ, s).

Русский

Шар единицы слева умножается на множество: ball(1, δ) * s = thickening(δ, s).

LaTeX

$$$$B(1,\delta) \cdot s = \operatorname{thickening}(\delta, s)$$$$

Lean4

@[to_additive]
theorem ball_mul_one : ball 1 δ * s = thickening δ s := by rw [mul_comm, mul_ball_one]

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

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

Разделы

Аффилиация

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