ContMDiff — Mathlib

English

A map is C^n on a manifold if it is C^n at every point of the domain, using the corresponding coordinate charts.

Русский

Отображение на многообразии является $C^n$ на всю область, если для каждой точки области оно является $C^n$ в соответствующих координатах.

LaTeX

$$ContMDiff\, n\, f = \forall x, ContMDiffAt\, I\, I'\, n\, f\, x$$

Lean4

/-- A function is `n` times continuously differentiable in a manifold if it is continuous
and, for any pair of points, it is `n` times continuously differentiable in the charts
around these points. -/
def ContMDiff (n : WithTop ℕ∞) (f : M → M') :=
  ∀ x, ContMDiffAt I I' n f x

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