English
In a seminormed commutative group, for every point x, radius δ, and set s, the product of the metric ball around x with s equals the left translate of the δ-thickening of s by x; i.e. Ball(x, δ) · s = x · Thickening(δ, s).
Русский
В семиномрированой абелевой группе для любой точки x, радиуса δ и множества s произведение шара β(x, δ) с множеством s равно левой сдвиговой телесности δ-множества s: Ball(x, δ) · s = x · Thickening(δ, s).
LaTeX
$$$\mathbb{B}(x, \delta) \cdot s = x \cdot \operatorname{thickening}(\delta, s)$$$
Lean4
@[to_additive (attr := simp)]
theorem ball_mul : ball x δ * s = x • thickening δ s := by rw [mul_comm, mul_ball]
