coordChange — Mathlib

English

If x lies in base sets of e and e', then the fiber coordinate-change map y ↦ e.coordChange e' (f y) (g y) is differentiable at x w.r.t. IM and the appropriate models.

Русский

Если x принадлежит базовым множествам e и e', то отображение волокна перехода координат y ↦ e.coordChange e' (f y) (g y) дифференцируемо в x относительно моделей IM.

LaTeX

$$$\displaystyle MDifferentiableAt IM 𝓘(\mathbb{K}, F) (\lambda y. e.coordChange e' (f y) (g y)) x.$$$

Lean4

protected theorem coordChange (hf : MDifferentiableAt IM IB f x) (hg : MDifferentiableAt IM 𝓘(𝕜, F) g x)
    (he : f x ∈ e.baseSet) (he' : f x ∈ e'.baseSet) :
    MDifferentiableAt IM 𝓘(𝕜, F) (fun y ↦ e.coordChange e' (f y) (g y)) x :=
  MDifferentiableWithinAt.coordChange hf hg he he'

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