coordChange — Mathlib

English

If a function f is differentiable on a set s, then the fiber coordinate-change map b ↦ e.coordChange e' (f b) (g b) is differentiable on s as a function into the space of linear endomorphisms.

Русский

Если функция f дифференцируема на множество s, переход координат волокна через e,e' дифференцируем на s как отображение в линейные эндоморфизмы.

LaTeX

$$$\displaystyle MDifferentiableOn IM IB (\lambda b. e.coordChange e' (f b) (g b)) \ s$$$

Lean4

protected theorem coordChange (hf : MDifferentiableOn IM IB f s) (hg : MDifferentiableOn IM 𝓘(𝕜, F) g s)
    (he : MapsTo f s e.baseSet) (he' : MapsTo f s e'.baseSet) :
    MDifferentiableOn IM 𝓘(𝕜, F) (fun y ↦ e.coordChange e' (f y) (g y)) s := fun x hx ↦
  (hf x hx).coordChange (hg x hx) (he hx) (he' hx)

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