mdifferentiable — Mathlib

English

A trivialization MDifferentiable between the product models yields MF-differentiability for the chart and its inverse.

Русский

Тривиализация, отображаемая взаимно дифференцируемо между произведениями моделей, даёт MF-дифференцируемость карты и её обратной карты.

LaTeX

$$Trivialization.mdifferentiable$$

Lean4

theorem mdifferentiable [ContMDiffVectorBundle 1 F Z I] (e : Trivialization F (π F Z)) [MemTrivializationAtlas e] :
    e.MDifferentiable (I.prod 𝓘(𝕜, F)) (I.prod 𝓘(𝕜, F)) :=
  ⟨e.contMDiffOn.mdifferentiableOn le_rfl, e.contMDiffOn_symm.mdifferentiableOn le_rfl⟩

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