English
If M is endowed with a charted-space structure via an open embedding e, and a map f composed with e has C^n regularity, then f itself has C^n regularity on its domain.
Русский
Если структура графового пространства M задана через открытое вложение e, и композиция e с f имеет гладкость C^n, то сама f имеет гладкость C^n.
LaTeX
$$$\text{If } e' \circ f \in C^n, \text{ then } f \in C^n.$$$
Lean4
/-- Let `M'` be a manifold whose chart structure is given by an open embedding `e'` into its model
space `H'`. If `e' ∘ f : M → H'` is `C^n`, then `f` is `C^n`.
This is useful, for example, when `e' ∘ f = g ∘ e` for smooth maps `e : M → X` and `g : X → H'`. -/
theorem of_comp_isOpenEmbedding {f : M → M'} (hf : ContMDiff I I' n (e' ∘ f)) :
haveI := h'.singletonChartedSpace;
ContMDiff I I' n f :=
by
have : f = (h'.toOpenPartialHomeomorph e').symm ∘ e' ∘ f :=
by
ext
rw [Function.comp_apply, Function.comp_apply, IsOpenEmbedding.toOpenPartialHomeomorph_left_inv]
rw [this]
apply
@ContMDiffOn.comp_contMDiff _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ h'.singletonChartedSpace _ _
(range e') _ (contMDiffOn_isOpenEmbedding_symm h') hf
simp
