toSphere_apply_aux — Mathlib

English

A technical equality relating the pushforward/pullback of μ to the unit sphere measure via a homeomorphism, describing how sets map under a spherical parametrization.

Русский

Техническое равенство, связывающее частичные отображения меры μ через сферическую параметризацию единичной сферы.

LaTeX

$$$\\mu\\bigl((\\uparrow)''(H^{-1}\\_\\text{s} \\times I^{}_o r)\\bigr) = \\mu\\bigl(I^{}_1 \\cdot (\\uparrow)''\\text{s}\\bigr)$$$

Lean4

theorem toSphere_apply_aux (s : Set (sphere (0 : E) 1)) (r : Ioi (0 : ℝ)) :
    μ ((↑) '' (homeomorphUnitSphereProd E ⁻¹' s ×ˢ Iio r)) = μ (Ioo (0 : ℝ) r • ((↑) '' s)) :=
  by
  rw [← image2_smul, image2_image_right, ← Homeomorph.image_symm, image_image, ← image_subtype_val_Ioi_Iio,
    image2_image_left, image2_swap, ← image_prod]
  rfl

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