preimage_mul_closedBall — Mathlib

English

Analogously, the preimage of a closedBall under left multiplication by b is the closedBall at a/b with radius r.

Русский

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

LaTeX

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

Lean4

@[to_additive (attr := simp high)]
theorem preimage_mul_closedBall (a b : E) (r : ℝ) : (b * ·) ⁻¹' closedBall a r = closedBall (a / b) r :=
  by
  ext c
  simp only [dist_eq_norm_div, Set.mem_preimage, mem_closedBall, div_div_eq_mul_div, mul_comm]

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