homeoRealMixedSpacePolarSpace_apply_fst_ofIsReal

English

If w is real, the first component of the image equals the original first component.

Русский

Если w реально, первая компонента образа равна исходной первой компоненте.

LaTeX

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

Lean4

theorem homeoRealMixedSpacePolarSpace_apply_fst_ofIsReal (x : realMixedSpace K) (w : { w // IsReal w }) :
    (homeoRealMixedSpacePolarSpace K x).1 w.1 = x.1 w := by
  simp_rw [homeoRealMixedSpacePolarSpace_apply, dif_pos w.prop]

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