English
For any x ∈ M, the chart at Sum.inl x is the lift along the inclusion to the left component of the chart at x: chartAt(H)(Sum.inl x) = (chartAt(H x)).lift_openEmbedding (X' := M ⊕ M') IsOpenEmbedding.inl.
Русский
Для любого x ∈ M карта по Sum.inl x равна ливингу по левому компоненту от карты chartAt(H x): chartAt(H)(Sum.inl x) = (chartAt(H x)).lift_openEmbedding (X' := M ⊕ M') IsOpenEmbedding.inl.
LaTeX
$$$chartAt\,H\,(\mathrm{Sum}.\mathrm{inl}\ x) = (chartAt\,H\ x).\mathrm{lift\_openEmbedding}\ (\mathrm{X'} := M \oplus M')\ \mathrm{IsOpenEmbedding.inl}.$$
Lean4
theorem sum_chartAt_inl (x : M) :
haveI : Nonempty H := nonempty_of_chartedSpace x
chartAt H (Sum.inl x) = (chartAt H x).lift_openEmbedding (X' := M ⊕ M') IsOpenEmbedding.inl :=
by
simp only [chartAt, sum, nonempty_of_chartedSpace x, ↓reduceDIte]
rfl
