contMDiffOn_one — Mathlib

English

Let I, I' be charted spaces and s ⊆ M. Then the constant map f: M → M' given by f(x) = 1 for all x is C^n on s, for every n.

Русский

Пусть I, I' задают графики пространства, и S ⊆ M. Тогда константная карта f: M → M', определяемая f(x) = 1 для всех x, является C^n на любой подмножине S (для любого n).

LaTeX

$$$\forall s \subseteq M,\ ContMDiffOn_I_I'_n(1 : M \to M')\,s$$$

Lean4

@[to_additive]
theorem contMDiffOn_one [One M'] : ContMDiffOn I I' n (1 : M → M') s :=
  contMDiff_one.contMDiffOn

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