smul_closedBall_one — Mathlib

English

Multiplication by x on a closed unit ball yields the closed ball around x: x • closedBall(1, δ) = closedBall(x, δ).

Русский

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

LaTeX

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

Lean4

@[to_additive (attr := simp 1100)]
theorem smul_closedBall_one : x • closedBall (1 : E) δ = closedBall x δ := by simp

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