measurable_polarCoordReal_symm — Mathlib

English

The determinant of FDerivPolarCoordRealSymm at x equals the product over complex places of the real part (x.snd w).

Русский

Определитель FDerivPolarCoordRealSymm в точке x равен произведению по комплексным местам действительной части x.snd w.

LaTeX

$$$\\det\\bigl(FDerivPolarCoordRealSymm\\;K\\;x\\bigr) = \\prod_{w: {w // IsComplex w}} (x.2 w).1$$$

Lean4

theorem measurable_polarCoordReal_symm : Measurable (polarCoordReal K).symm :=
  by
  refine measurable_fst.prodMk <| Measurable.comp ?_ measurable_snd
  exact measurable_pi_lambda _ fun _ ↦ continuous_polarCoord_symm.measurable.comp (measurable_pi_apply _)

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