contMDiffWithinAt_const — Mathlib

English

For any s ⊆ M, the constant map f ≡ 1 is C^n on s in the ContMDiff sense at every x ∈ s.

Русский

Для любой подмножества s ⊆ M константная карта f ≡ 1 является C^n на s в смысле ContMDiff в каждой точке x ∈ s.

LaTeX

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

Lean4

theorem contMDiffWithinAt_const : ContMDiffWithinAt I I' n (fun _ : M => c) s x :=
  contMDiffAt_const.contMDiffWithinAt

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