homeoRealMixedSpacePolarSpace_apply_snd

English

The second component of the image under the real-mixed space to polar space homeomorphism is given by the original second component.

Русский

Вторая компонентa образа под гомеоморфизмом задаётся исходной второй компонентой.

LaTeX

$$$(\\mathrm{homeoRealMixedSpacePolarSpace}(K)\\ x)_{2} \\ w = (x.2 w).2$$$

Lean4

theorem homeoRealMixedSpacePolarSpace_apply_snd (x : realMixedSpace K) (w : { w // IsComplex w }) :
    (homeoRealMixedSpacePolarSpace K x).2 w = (x.2 w).2 :=
  rfl

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