homeoRealMixedSpacePolarSpace_symm_apply

English

If w is complex, the first component of the image equals the real part of the second mixed component.

Русский

Если w комплексно, первая компонента образа равна вещественной части второй компоненты смешанного пространства.

LaTeX

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

Lean4

@[simp]
theorem homeoRealMixedSpacePolarSpace_symm_apply (x : polarSpace K) :
    (homeoRealMixedSpacePolarSpace K).symm x = ⟨fun w ↦ x.1 w, fun w ↦ (x.1 w, x.2 w)⟩ :=
  rfl

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