measurableEquivRealProd_symm_polarCoord_symm_apply

English

The two natural inverses used to recover complex numbers from polar coordinates agree. Equivalently, the inverse map coming from the real–product equivalence coincides with the standard Complex polar coordinate inverse at every point p ∈ ℝ × ℝ.

Русский

Две естественные обратные карты, используемые для восстановления комплексного числа по полярным координатам, совпадают. Эквивалентно, обратная карта, заданная через эквивалентность ℝ×ℝ, совпадает с обычной обратной полярной картой Complex при любом p ∈ ℝ×ℝ.

LaTeX

$$$\forall p \in \mathbb{R} \times \mathbb{R},\quad \mathrm{measurableEquivRealProd.symm}(\mathrm{polarCoord.symm}(p)) = \mathrm{Complex.polarCoord.symm}(p).$$$

Lean4

theorem measurableEquivRealProd_symm_polarCoord_symm_apply (p : ℝ × ℝ) :
    (measurableEquivRealProd.symm (polarCoord.symm p)) = Complex.polarCoord.symm p :=
  rfl

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