preimage_mul_sphere — Mathlib

English

Left multiplication by b maps the sphere around a with radius r to the sphere around a/b with radius r.

Русский

Левая передвижка на b переносит сферу вокруг a радиуса r в сферу вокруг a/b радиуса r.

LaTeX

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

Lean4

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

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