polarCoordReal — Mathlib

English

The mixedEmbedding.polarCoord is symmetry-equivalent to the composition of identifications.

Русский

Полярная координата смешанного вложения эквивалентна композиции идентификаторов.

LaTeX

$$$(mixedEmbedding.polarCoord(K)).symm = (mixedSpaceToRealMixedSpace(K)).symm \\circ (polarCoordReal(K)).symm$$$

Lean4

/-- The polar coordinate open partial homeomorphism of `ℝ^r₁ × (ℝ × ℝ)^r₂` defined as the identity on
the first component and mapping `(rᵢ cos θᵢ, rᵢ sin θᵢ)ᵢ` to `(rᵢ, θᵢ)ᵢ` on the second component.
-/
@[simps! apply target]
def polarCoordReal : OpenPartialHomeomorph (realMixedSpace K) (realMixedSpace K) :=
  (OpenPartialHomeomorph.refl _).prod (OpenPartialHomeomorph.pi fun _ ↦ polarCoord)

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