contMDiffAt_of_subsingleton

Mathlib.Geometry.Manifold.ContMDiff.Basic

URI: https://scilib.ai/kg/mathlib#contMDiffAt_of_subsingleton

English

If M' is a subsingleton, then ContMDiffAt I I' n f x holds for every f and every x.

Русский

Если M' является одиночным множеством, то ContMDiffAt I I' n f x выполняется для любой f и любой x.

LaTeX

$$$[Subsingleton M']\Rightarrow ContMDiffAt_I_I'_n f x$$$

Lean4

@[nontriviality]
theorem contMDiffAt_of_subsingleton [Subsingleton M'] : ContMDiffAt I I' n f x :=
  contMDiff_of_subsingleton.contMDiffAt

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

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

Разделы

Аффилиация

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