coordChangeL — Mathlib

English

The coordChangeL map is ContMDiffAt with respect to the base, i.e., its dependence on the base point is C^n at the point x.

Русский

Координатное преобразование гладко по базисной точке x.

LaTeX

$$$\operatorname{ContMDiffAt} IM IB n (e.coordChangeL 𝕜 e' (f y)) x$$$

Lean4

protected theorem coordChangeL (hf : ContMDiffWithinAt IM IB n f s x) (he : f x ∈ e.baseSet) (he' : f x ∈ e'.baseSet) :
    ContMDiffWithinAt IM 𝓘(𝕜, F →L[𝕜] F) n (fun y ↦ (e.coordChangeL 𝕜 e' (f y) : F →L[𝕜] F)) s x :=
  (contMDiffAt_coordChangeL he he').comp_contMDiffWithinAt _ hf

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