English
A map is of class C^n on a set if it is continuous at every point of the set and, at each point, its coordinate expression is C^n in the chart around that point.
Русский
Отображение принадлежит классу $C^n$ на множестве, если оно непрерывно в каждой точке множества и в каждой точке в соответствующей системе координат координатное выражение принадлежит классу $C^n$.
LaTeX
$$$ContMDiffOn\, n\, f\, s = \forall x \in s,\ ContMDiffWithinAt\, I\, I'\, n\, f\, s\, x$$
Lean4
/-- A function is `n` times continuously differentiable in a set of a manifold if it is continuous
and, for any pair of points, it is `n` times continuously differentiable on this set in the charts
around these points. -/
def ContMDiffOn (n : WithTop ℕ∞) (f : M → M') (s : Set M) :=
∀ x ∈ s, ContMDiffWithinAt I I' n f s x
