polarCoord — Mathlib

English

The image of the target under polarCoordReal.symm equals the universal set almost everywhere with respect to volume.

Русский

Образ целевого множества под polarCoordReal.symm совпадает с всеобщим почти всюду по объёму.

LaTeX

$$$\\operatorname{polarCoordReal\_symm\_target\_ae\_eq\_univ}(K):\\; (polarCoordReal(K).symm\\,''\\; (polarCoordReal(K).target)) =^{ae}_{volume} \\mathrm{Set.univ}$$$

Lean4

/-- The polar coordinate open partial homeomorphism between the mixed space `ℝ^r₁ × ℂ^r₂` and
`ℝ^r₁ × (ℝ × ℝ)^r₂` defined as the identity on the first component and mapping `(zᵢ)ᵢ` to
`(‖zᵢ‖, Arg zᵢ)ᵢ` on the second component.
-/
@[simps!]
protected noncomputable def polarCoord : OpenPartialHomeomorph (mixedSpace K) (realMixedSpace K) :=
  (OpenPartialHomeomorph.refl _).prod (OpenPartialHomeomorph.pi fun _ ↦ Complex.polarCoord)

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