contMDiffWithinAt_of_subsingleton

English

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

Русский

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

LaTeX

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

Lean4

@[nontriviality]
theorem contMDiffWithinAt_of_subsingleton [Subsingleton M'] : ContMDiffWithinAt I I' n f s x :=
  contMDiffAt_of_subsingleton.contMDiffWithinAt

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