homeoRealMixedSpacePolarSpace_apply_fst_ofIsComplex

English

The inverse of the real-mixed space to polar space homeomorphism sends a polar point back to the canonical pair.

Русский

Обратное отображение возвращает полярную точку к канонической паре.

LaTeX

$$$\\text{(homeoRealMixedSpacePolarSpace}(K))^{-1}(x) = \\langle f, g \\rangle$ with $f(w) = x.1 w$, $g(w) = (x.1 w, x.2 w) $$$

Lean4

theorem homeoRealMixedSpacePolarSpace_apply_fst_ofIsComplex (x : realMixedSpace K) (w : { w // IsComplex w }) :
    (homeoRealMixedSpacePolarSpace K x).1 w.1 = (x.2 w).1 := by
  simp_rw [homeoRealMixedSpacePolarSpace_apply, dif_neg (not_isReal_iff_isComplex.mpr w.prop)]

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