singleton_mul_closedBall_one — Mathlib

English

Multiplication by a singleton with the unit ball yields the closed ball around x: {x} * closedBall(1, δ) = closedBall(x, δ).

Русский

Умножение единичного множества на замкнутый шар даёт шар вокруг x: {x} * closedBall(1, δ) = closedBall(x, δ).

LaTeX

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

Lean4

@[to_additive]
theorem singleton_mul_closedBall_one : { x } * closedBall 1 δ = closedBall x δ := by simp

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