English
If e : M → H is an open embedding, then its inverse e^{-1} : range(e) → M is C^n for every n.
Русский
Если e : M → H — открытое вложение, то обратная карта e^{-1}: range(e) → M гладкая до степени n для любого n.
LaTeX
$$$e^{-1}: \mathrm{range}(e) \to M$ 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 the inverse of `e` is `C^n`. -/
theorem contMDiffOn_isOpenEmbedding_symm [Nonempty M] :
haveI := h.singletonChartedSpace;
ContMDiffOn I I n (IsOpenEmbedding.toOpenPartialHomeomorph e h).symm (range e) :=
by
haveI := h.isManifold_singleton (I := I) (n := ω)
rw [@contMDiffOn_iff]
constructor
· rw [← h.toOpenPartialHomeomorph_target]
exact (h.toOpenPartialHomeomorph e).continuousOn_symm
· intro z hz
apply contDiffOn_id.congr
intro z hz
simp only [mfld_simps]
have : I.symm z ∈ range e := by
rw [ModelWithCorners.symm, ← mem_preimage]
exact hz.2.1
rw [h.toOpenPartialHomeomorph_right_inv e this]
apply I.right_inv
exact mem_of_subset_of_mem (extChartAt_target_subset_range _) hz.1
