mdifferentiable' — Mathlib

English

If s is a C^n-section with n ≥ 1, then the map x ↦ TotalSpace.mk' F x (s x) is differentiable in the MDifferentiable sense along the product with the model I.

Русский

Если s — секция класса C^n с n ≥ 1, то отображение x ↦ TotalSpace.mk' F x (s x) дифференцируемо в смысле MDifferentiable вдоль произведения с моделью I.

LaTeX

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

Lean4

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

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