English
The injection Sum.inl: M → M ⊕ M' is ContMDiff.
Русский
Инъекция Sum.inl: M → M ⊕ M' гладкая.
LaTeX
$$$ ContMDiff I I n Sum.inl $$$
Lean4
theorem inl : ContMDiff I I n (@Sum.inl M M') := by
intro x
rw [contMDiffAt_iff]
refine
⟨continuous_inl.continuousAt, ?_⟩
-- In extended charts, .inl equals the identity (on the chart sources).
apply contDiffWithinAt_id.congr_of_eventuallyEq; swap
· simp [ChartedSpace.sum_chartAt_inl]
congr
apply Sum.inl_injective.extend_apply (chartAt _ x)
set C := chartAt H x with hC
have : I.symm ⁻¹' C.target ∩ range I ∈ 𝓝[range I] (extChartAt I x) x :=
by
rw [← I.image_eq (chartAt H x).target]
exact (chartAt H x).extend_image_target_mem_nhds (mem_chart_source _ x)
filter_upwards [this] with y hy
simp [extChartAt, sum_chartAt_inl, ← hC, Sum.inl_injective.extend_apply C, C.right_inv hy.1, I.right_inv hy.2]
