English
If f is MDifferentiableWithinAt and the base point x lies in both base sets, then the coordinate-change map b ↦ (e.coordChange L or coordChange) is differentiable within s at x into the linear endomorphisms of F.
Русский
Если f дифференцируемая внутри s и x лежит в базовых множествах, переход координат через e,e' дифференцируем внутри s в x как отображение в линейные отображения F.
LaTeX
$$$\displaystyle MDifferentiableWithinAt IM 𝓘(\mathbb{K}, F) (\lambda b. (e.coordChange e' (f b) (g b)) ) s x.$$$
Lean4
protected theorem coordChange (hf : MDifferentiableWithinAt IM IB f s x) (hg : MDifferentiableWithinAt IM 𝓘(𝕜, F) g s x)
(he : f x ∈ e.baseSet) (he' : f x ∈ e'.baseSet) :
MDifferentiableWithinAt IM 𝓘(𝕜, F) (fun y ↦ e.coordChange e' (f y) (g y)) s x :=
by
refine ((hf.coordChangeL he he').clm_apply hg).congr_of_eventuallyEq ?_ ?_
· have : e.baseSet ∩ e'.baseSet ∈ 𝓝 (f x) := (e.open_baseSet.inter e'.open_baseSet).mem_nhds ⟨he, he'⟩
filter_upwards [hf.continuousWithinAt this] with y hy
exact (Trivialization.coordChangeL_apply' e e' hy (g y)).symm
· exact (Trivialization.coordChangeL_apply' e e' ⟨he, he'⟩ (g x)).symm
