mul_mem_closedBall_iff_norm — Mathlib

English

Similarly, left translation by b preserves closed balls: a·b ∈ closedBall a r iff ‖b‖ ≤ r.

Русский

Аналогично для закрытого шара: a·b принадлежит closedBall(a,r) тогда и только тогда, когда ‖b‖ ≤ r.

LaTeX

$$$\displaystyle a\cdot b \in \mathrm{closedBall}\,a\,r \iff \|b\| \le r$$$

Lean4

@[to_additive]
theorem mul_mem_closedBall_iff_norm : a * b ∈ closedBall a r ↔ ‖b‖ ≤ r := by
  rw [mem_closedBall_iff_norm'', mul_div_cancel_left]
    -- Higher priority to apply this before the equivalent lemma `Metric.preimage_mul_left_ball`.

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