English
The injection Sum.inr: M' → M ⊕ M' is ContMDiff.
Русский
Инъекция Sum.inr: M' → M ⊕ M' гладкая.
LaTeX
$$$ ContMDiff I I n Sum.inr $$$
Lean4
theorem inr : ContMDiff I I n (@Sum.inr M M') := by
intro x
rw [contMDiffAt_iff]
refine
⟨continuous_inr.continuousAt, ?_⟩
-- In extended charts, .inl equals the identity (on the chart sources).
apply contDiffWithinAt_id.congr_of_eventuallyEq; swap
· simp only [mfld_simps, sum_chartAt_inr]
congr
apply Sum.inr_injective.extend_apply (chartAt _ x)
set C := chartAt H x with hC
have : I.symm ⁻¹' (chartAt H x).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_inr, ← hC, Sum.inr_injective.extend_apply C, C.right_inv hy.1, I.right_inv hy.2]
