mul_ball

Mathlib.Analysis.Normed.Group.Pointwise

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

English

For any set s and any x, s * ball x δ equals x • thickening δ s: s * Ball(x, δ) = x • Thickening(δ, s).

Русский

Для множества s и любого x, s * Ball(x, δ) = x • Thickening(δ, s).

LaTeX

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

Lean4

@[to_additive (attr := simp)]
theorem mul_ball : s * ball x δ = x • thickening δ s := by rw [← smul_ball_one, mul_smul_comm, mul_ball_one]

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

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

Разделы

Аффилиация

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