English
Let f: M → M' be a map between manifolds with corners. If for every point x ∈ M there exists an open neighborhood U of x such that the restriction f|_U is ContMDiff of order n (with respect to I and I'), then f is ContMDiff of order n on all of M.
Русский
Пусть f: M → M' — отображение между многообразиями с углами. Если для каждой точки x ∈ M существует открытая окрестность U так, что ограничение f|_U является ContMDiff порядка n (с учётом структур I и I'), то f является ContMDiff порядка n на всей M.
LaTeX
$$$\left(\forall x \in M, \; \exists U \text{ открытое}, x \in U \land \ContMDiffOn I I' n f U\right) \Rightarrow \ContMDiff I I' n f$$$
Lean4
theorem contMDiff_of_locally_contMDiffOn (h : ∀ x, ∃ u, IsOpen u ∧ x ∈ u ∧ ContMDiffOn I I' n f u) :
ContMDiff I I' n f :=
(contDiffWithinAt_localInvariantProp n).liftProp_of_locally_liftPropOn h
