mixedSpaceToRealMixedSpace_apply — Mathlib

English

The map real-polar coordinate decomposition acts componentwise as identity on the first factor and uses Complex.polarCoord on the second.

Русский

Полярная координатная декомпозиция действует по компонентам: на первой координате — тождество, на второй — Complex.polarCoord.

LaTeX

$$$\\text{mixedSpaceToRealMixedSpace}(K)(x) = \\bigl( x_1, \\lambda w. \\text{Complex.equivRealProd}(x_2(w)) \\bigr).$$$

Lean4

@[simp]
theorem mixedSpaceToRealMixedSpace_apply (x : mixedSpace K) :
    mixedSpaceToRealMixedSpace K x = (x.1, fun w ↦ Complex.equivRealProd (x.2 w)) :=
  rfl

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