contMDiffWithinAt_one — Mathlib

English

Let [One M'] hold. Then for any x ∈ M, the map x ↦ 1 is ContMDiffAt I I' n at x.

Русский

Пусть существует единица в M'. Тогда для любой точки x ∈ M отображение x ↦ 1 является ContMDiffAt в точке x.

LaTeX

$$$\forall x\in M,\ ContMDiffAt_I_I'_n(1 : M \to M')\ x$$$

Lean4

@[to_additive]
theorem contMDiffWithinAt_one [One M'] : ContMDiffWithinAt I I' n (1 : M → M') s x :=
  contMDiffAt_const.contMDiffWithinAt

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