hasMFDerivAt_extChartAt — Mathlib

English

If e is MDifferentiable from I to I' and e' is MDifferentiable from I' to I'', then the composition e.trans e' is MDifferentiable from I to I''.

Русский

Если e дифференцируемо от I к I' и e' дифференцируемо от I' к I'', то композиция e.trans e' дифференцируема от I к I''.

LaTeX

$$$\text{MDifferentiable}(I,I',e) \rightarrow \text{MDifferentiable}(I',I'',e') \rightarrow \text{MDifferentiable}(I,I'',e.trans e')$$$

Lean4

theorem hasMFDerivAt_extChartAt (h : y ∈ (chartAt H x).source) :
    HasMFDerivAt I 𝓘(𝕜, E) (extChartAt I x) y (mfderiv I I (chartAt H x) y :) :=
  I.hasMFDerivAt.comp y ((mdifferentiable_chart x).mdifferentiableAt h).hasMFDerivAt

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