mul_mem_closedBall_mul_iff — Mathlib

English

For any a,b in a seminormed group and any c, the closed ball around a shifted by c is equivalent to the closed ball around a·c with the same center scaled accordingly: dist-based equivalence with div, etc.

Русский

Для любых a, b и c в полугруппе с нормой шар вокруг a, смещённый на c, эквивалентен шаром вокруг a·c по той же шкале.

LaTeX

$$$\displaystyle a\cdot c\in \mathrm{closedBall}(\,b\cdot c\, , r) \iff a\in \mathrm{closedBall}(b,r) $$$

Lean4

@[to_additive]
theorem mul_mem_closedBall_mul_iff {c : E} : a * c ∈ closedBall (b * c) r ↔ a ∈ closedBall b r := by
  simp only [mem_closedBall, dist_eq_norm_div, mul_div_mul_right_eq_div]

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