English
At a fixed base point x, the map b ↦ (e.coordChangeL 𝕜 e' (f x)) is C^n in the parameter b, i.e., the fiber coordinate change is smooth as a function of the base point.
Русский
В точке основания отображение b ↦ e.coordChangeL гладко по параметру b.
LaTeX
$$$\operatorname{ContMDiffAt} IB n (\lambda b, (e.coordChangeL 𝕜 e' b)) x$$$
Lean4
theorem contMDiffAt_coordChangeL {x : B} (h : x ∈ e.baseSet) (h' : x ∈ e'.baseSet) :
ContMDiffAt IB 𝓘(𝕜, F →L[𝕜] F) n (fun b : B => (e.coordChangeL 𝕜 e' b : F →L[𝕜] F)) x :=
(contMDiffOn_coordChangeL e e').contMDiffAt <| (e.open_baseSet.inter e'.open_baseSet).mem_nhds ⟨h, h'⟩