English
If a charted-space structure on M is given by an open embedding e : M → H, then e is C^n for every n; i.e., the embedding is as smooth as desired.
Русский
Если структура графовой пространства M задана открытым вложением e: M → H, то e гладко класса C^n для любого n; то есть вложение гладкое на любом уровне.
LaTeX
$$$e: M \to H$ is of class $C^n$ for all integers n.$$
Lean4
/-- If the `ChartedSpace` structure on a manifold `M` is given by an open embedding `e : M → H`,
then `e` is `C^n`. -/
theorem contMDiff_isOpenEmbedding [Nonempty M] :
haveI := h.singletonChartedSpace;
ContMDiff I I n e :=
by
haveI := h.isManifold_singleton (I := I) (n := ω)
rw [@contMDiff_iff _ _ _ _ _ _ _ _ _ _ h.singletonChartedSpace]
use h.continuous
intro x y
apply contDiffOn_id.congr
intro z hz
simp only [mfld_simps]
rw [h.toOpenPartialHomeomorph_right_inv]
· rw [I.right_inv]
apply mem_of_subset_of_mem _ hz.1
exact
letI := h.singletonChartedSpace;
extChartAt_target_subset_range (I := I) x
· -- `hz` implies that `z ∈ range (I ∘ e)`
have := hz.1
rw [@extChartAt_target _ _ _ _ _ _ _ _ _ _ h.singletonChartedSpace] at this
have := this.1
rw [mem_preimage, OpenPartialHomeomorph.singletonChartedSpace_chartAt_eq, h.toOpenPartialHomeomorph_target] at this
exact this
