coordChangeL — Mathlib

English

If f is C^n on a set, then the fiber-coordinates coordinate-change map is C^n as a function on the base, restricted to that set.

Русский

Если функция гладкая на некотором множестве, то переход координат волокна относительно этой области гладок.

LaTeX

$$$\operatorname{contMDiffWithinAt} IM IB n f s x \Rightarrow \dots$$$

Lean4

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

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