singleton_mul_closedBall — Mathlib

English

Left multiplying a singleton by a closed ball yields the closed ball around the product: {x} * closedBall(y, δ) = closedBall(xy, δ).

Русский

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

LaTeX

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

Lean4

@[to_additive (attr := simp 1100)]
theorem singleton_mul_closedBall : { x } * closedBall y δ = closedBall (x * y) δ := by
  simp_rw [singleton_mul, ← smul_eq_mul, image_smul, smul_closedBall]

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