English
If f and g are ContMDiff, then Sum.elim f g is ContMDiff.
Русский
Если f и g гладкие, то Sum.elim f g гладкое.
LaTeX
$$$ (\ContMDiff I J n f) \land (\ContMDiff I J n g) \Rightarrow \ContMDiff I J n (Sum.elim f g) $$$
Lean4
theorem sumElim {f : M → N} {g : M' → N} (hf : ContMDiff I J n f) (hg : ContMDiff I J n g) :
ContMDiff I J n (Sum.elim f g) := by
intro p
rw [contMDiffAt_iff]
refine ⟨(Continuous.sumElim hf.continuous hg.continuous).continuousAt, ?_⟩
cases p with
| inl x =>
-- In charts around x : M, the map f ⊔ g looks like f.
-- This is how they both look like in extended charts.
have :
ContDiffWithinAt 𝕜 n ((extChartAt J (f x)) ∘ f ∘ (extChartAt I x).symm) (range I)
((extChartAt I (.inl x : M ⊕ M')) (Sum.inl x)) :=
by
let hf' := hf x
rw [contMDiffAt_iff] at hf'
simpa using hf'.2
apply this.congr_of_eventuallyEq
· simp only [extChartAt, Sum.elim_inl, ChartedSpace.sum_chartAt_inl]
filter_upwards with a
congr
· -- They agree at the image of x.
simp only [extChartAt, ChartedSpace.sum_chartAt_inl, Sum.elim_inl]
congr
| inr x =>
-- In charts around x : M, the map f ⊔ g looks like g.
-- This is how they both look like in extended charts.
have :
ContDiffWithinAt 𝕜 n ((extChartAt J (g x)) ∘ g ∘ (extChartAt I x).symm) (range I)
((extChartAt I (.inr x : M ⊕ M')) (Sum.inr x)) :=
by
let hg' := hg x
rw [contMDiffAt_iff] at hg'
simpa using hg'.2
apply this.congr_of_eventuallyEq
· simp only [extChartAt, Sum.elim_inr, ChartedSpace.sum_chartAt_inr]
filter_upwards with a
congr
· -- They agree at the image of x.
simp only [extChartAt, ChartedSpace.sum_chartAt_inr, Sum.elim_inr]
congr
