mul_mem_ball_mul_iff — Mathlib

English

Analogous to the previous lemma, left-multiplication by c preserves ball structure: a·c ∈ ball (b·c) r ↔ a ∈ ball b r.

Русский

Аналогично предыдущему лемме: левое умножение на c сохраняет шаровую структуру: a·c ∈ ball (b·c) r ⇔ a ∈ ball b r.

LaTeX

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

Lean4

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

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