mdifferentiable — Mathlib

English

For sufficiently smooth sections, the lifted total-space map x ↦ TotalSpace.mk' F x (s x) is MDifferentiable with respect to I and the product model.

Русский

Для достаточно гладких секций отображение в обобщенном пространстве x ↦ TotalSpace.mk' F x (s x) дифференцируемо в смысле MDifferentiable относительно I и произведения моделей.

LaTeX

$$$$ MDifferentiable I (I.\!\mathrm{prod}} (\mathcal{I}(\mathbb{K},F)) \big( x \mapsto \mathrm{TotalSpace.mk}' F x (s x) \big) $$$$

Lean4

protected theorem mdifferentiable (s : Cₛ^∞⟮I; F, V⟯) :
    MDifferentiable I (I.prod 𝓘(𝕜, F)) fun x => TotalSpace.mk' F x (s x : V x) :=
  s.contMDiff.mdifferentiable (mod_cast le_top)

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