English
If g is ContMDiffWithinAt on t and f is ContMDiffWithinAt on s and MapsTo f s t, then g∘f is ContMDiffWithinAt on s.
Русский
Если g C^n внутри t, f C^n внутри s и f сохраняет S→t, то композиция g∘f C^n внутри s.
LaTeX
$$$hg: ContMDiffWithinAt I' I'' n g t, \\\\ hf: ContMDiffWithinAt I I' n f s x, \\\\ st: MapsTo f s t \\\\Rightarrow ContMDiffWithinAt I I'' n (g \\circ f) s x$$$
Lean4
/-- The composition of `C^n` functions within domains at points is `C^n`. -/
theorem comp {t : Set M'} {g : M' → M''} (x : M) (hg : ContMDiffWithinAt I' I'' n g t (f x))
(hf : ContMDiffWithinAt I I' n f s x) (st : MapsTo f s t) : ContMDiffWithinAt I I'' n (g ∘ f) s x :=
by
rw [contMDiffWithinAt_iff] at hg hf ⊢
refine ⟨hg.1.comp hf.1 st, ?_⟩
set e := extChartAt I x
set e' := extChartAt I' (f x)
have : e' (f x) = (writtenInExtChartAt I I' x f) (e x) := by simp only [e, e', mfld_simps]
rw [this] at hg
have A : ∀ᶠ y in 𝓝[e.symm ⁻¹' s ∩ range I] e x, f (e.symm y) ∈ t ∧ f (e.symm y) ∈ e'.source :=
by
simp only [e, ← map_extChartAt_nhdsWithin, eventually_map]
filter_upwards [hf.1.tendsto (extChartAt_source_mem_nhds (I := I') (f x)),
inter_mem_nhdsWithin s (extChartAt_source_mem_nhds (I := I) x)]
rintro x' (hfx' : f x' ∈ e'.source) ⟨hx's, hx'⟩
simp only [e, true_and, e.left_inv hx', st hx's, *]
refine
((hg.2.comp _ (hf.2.mono inter_subset_right)
((mapsTo_preimage _ _).mono_left inter_subset_left)).mono_of_mem_nhdsWithin
(inter_mem ?_ self_mem_nhdsWithin)).congr_of_eventuallyEq
?_ ?_
· filter_upwards [A]
rintro x' ⟨ht, hfx'⟩
simp only [*, e, e', mem_preimage, writtenInExtChartAt, (· ∘ ·), mem_inter_iff, e'.left_inv, true_and]
exact mem_range_self _
· filter_upwards [A]
rintro x' ⟨-, hfx'⟩
simp only [*, e, e', (· ∘ ·), writtenInExtChartAt, e'.left_inv]
· simp only [e, e', writtenInExtChartAt, (· ∘ ·), mem_extChartAt_source, e.left_inv, e'.left_inv]
