instDFunLike — Mathlib

English

If s is a smooth section of the vector bundle, then the map x ↦ TotalSpace.mk' F x (s(x)) is C^k as a map M → TotalSpace F.

Русский

Если s — гладкая секция векторного расслоения, то отображение x ↦ TotalSpace.mk' F x (s(x)) является C^k как отображение M в TotalSpace F.

LaTeX

$$$\text{ContMDiffSection I F n V} \;s \Rightarrow \ ContMDiff I (I.prod (modelWithCornersSelf 𝕜 F)) n (x \mapsto TotalSpace.mk' F x (s(x))).$$$

Lean4

instance : DFunLike Cₛ^n⟮I; F, V⟯ M V where
  coe := ContMDiffSection.toFun
  coe_injective' := by rintro ⟨⟩ ⟨⟩ h; congr

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