coordChangeL — Mathlib

English

If x lies in the base sets of two trivializations e and e', then the coordinate-change map b ↦ (e.coordChangeL 𝕜 e' b) is differentiable at x with respect to the model 𝓘(𝕜, F →L[𝕜] F).

Русский

Если x принадлежит базовым множествам двух тривиализаций e и e', то отображение b ↦ (e.coordChangeL 𝕜 e' b) дифференцируемо в x в модели 𝓘(𝕜, F →L[𝕜] F).

LaTeX

$$$\displaystyle MDifferentiableAt\!\; IB \, \mathcal{I}(\mathbb{K}, F \to_L[\mathbb{K}] F)\; (\lambda b: B. (e.coordChangeL 𝕜 e' b : F \to_L[\mathbb{K}] F))\ x,$$$

Lean4

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

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