contMDiff

Mathlib.Geometry.Manifold.ContMDiffMap

URI: https://scilib.ai/kg/mathlib#ContMDiffMap.contMDiff

English

If f is a bundled C^n map, then its underlying function is a C^n map.

Русский

При наличии упакованного C^n отображения, соответствующая функция является C^n отображением.

LaTeX

$$$\forall f:\, C^n⟮I, M; I', M'⟯,\; ContMDiff I I' n (ContMDiffMap.instFunLike.coe f)$$$

Lean4

protected theorem contMDiff (f : C^n⟮I, M; I', M'⟯) : ContMDiff I I' n f :=
  f.prop

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru