mdifferentiable — Mathlib

English

A ContMDiffMap has a differentiability property at a point x for the underlying map.

Русский

У ContMDiffMap есть свойство дифференцируемости в точке в основе отображения.

LaTeX

$$$\forall f : ContMDiffMap I I' M M' (WithTop.some instTopENat.top),\; MDifferentiable I I' (ContMDiffMap.instFunLike.coe f)$$$

Lean4

protected theorem mdifferentiable (f : C^∞⟮I, M; I', M'⟯) : MDifferentiable I I' f :=
  f.contMDiff.mdifferentiable (mod_cast le_top)

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