preimage_mul_ball — Mathlib

English

For left multiplication by b, the preimage of the ball around a with radius r is the ball around a/b with radius r.

Русский

При левом умножении на b прообраз шара вокруг a радиуса r равен шару вокруг a/b радиуса r.

LaTeX

$$$\displaystyle (b\cdot\,\cdot)^{-1}'\mathrm{ball}\,a\,r = \mathrm{ball}\,(a/b)\,r$$$

Lean4

@[to_additive (attr := simp high)]
theorem preimage_mul_ball (a b : E) (r : ℝ) : (b * ·) ⁻¹' ball a r = ball (a / b) r :=
  by
  ext c
  simp only [dist_eq_norm_div, Set.mem_preimage, mem_ball, div_div_eq_mul_div, mul_comm]
    -- Higher priority to apply this before the equivalent lemma `Metric.preimage_mul_left_closedBall`.

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