singleton_mul_ball — Mathlib

English

In a seminormed commutative group, left translation by a fixed element x sends the ball around y to the ball around xy with the same radius: {x} * ball(y, δ) = ball(xy, δ).

Русский

В полугруппе с нормировкой слева перенос по фиксированному элементу x отправляет шар вокруг y в шар вокруг xy той же радиуса: {x} * ball(y, δ) = ball(xy, δ).

LaTeX

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

Lean4

@[to_additive]
theorem singleton_mul_ball : { x } * ball y δ = ball (x * y) δ := by
  simp only [preimage_mul_ball, image_mul_left, singleton_mul, div_inv_eq_mul, mul_comm y x]

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