polarCoordReal_symm_target_ae_eq_univ

English

The action of polarCoordReal on x is given by (x.1, w ↦ Complex.equivRealProd(x.2 w)).

Русский

Действие polarCoordReal на x задаётся как (x.1, w ↦ Complex.equivRealProd(x.2 w)).

LaTeX

$$$\\text{polarCoordReal}(K)(x) = \\bigl(x.1, \\lambda w. \\operatorname{Complex.equivRealProd}(x.2 w)\\bigr)$.$$

Lean4

theorem polarCoordReal_symm_target_ae_eq_univ :
    (polarCoordReal K).symm '' (polarCoordReal K).target =ᵐ[volume] Set.univ :=
  by
  rw [← Set.univ_prod_univ, volume_eq_prod, (polarCoordReal K).symm_image_target_eq_source, polarCoordReal_source, ←
    polarCoord.symm_image_target_eq_source, ← Set.piMap_image_univ_pi]
  exact set_prod_ae_eq .rfl pi_polarCoord_symm_target_ae_eq_univ

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