contMDiffOn_coordChangeL — Mathlib

English

The coordChange between two trivializations is ContMDiffAt in the base point x, i.e., differentiable with respect to the base parameter.

Русский

Переход координат между тривиализациями гладок в точке основания.

LaTeX

$$$\operatorname{contMDiff_coordChange} \; hf\; hg\; \dots$$$

Lean4

theorem contMDiffOn_coordChangeL :
    ContMDiffOn IB 𝓘(𝕜, F →L[𝕜] F) n (fun b : B => (e.coordChangeL 𝕜 e' b : F →L[𝕜] F)) (e.baseSet ∩ e'.baseSet) :=
  ContMDiffVectorBundle.contMDiffOn_coordChangeL e e'

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