English
For x,y ∈ M, the evaluation of the left chart in the Sum space coincides with the evaluation of the left factor chart: ((chartAt H (Sum.inl x)).toFun' (Sum.inl y)) = ((chartAt H x).toFun') y.
Русский
Для x,y ∈ M, применение левой карты в суммарном пространстве совпадает с применением карты левой компоненты: ((chartAt H (Sum.inl x)).toFun' (Sum.inl y)) = ((chartAt H x).toFun') y.
LaTeX
$$$\big((chartAt\,H\,(\mathrm{Sum}.\mathrm{inl}\ x)).\mathrm{toFun'}\ (\mathrm{Sum}.\mathrm{inl}\ y)\big) = (chartAt\,H\ x).\mathrm{toFun'}\ y$$$
Lean4
@[simp, mfld_simps]
theorem sum_chartAt_inl_apply {x y : M} : (chartAt H (.inl x : M ⊕ M')) (Sum.inl y) = (chartAt H x) y :=
by
haveI : Nonempty H := nonempty_of_chartedSpace x
rw [ChartedSpace.sum_chartAt_inl]
exact OpenPartialHomeomorph.lift_openEmbedding_apply _ _
