contMDiffAt_coordChangeL — Mathlib

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'⟩

Похожие утверждения