isManifold_singleton — Mathlib

English

If f is an open embedding, the singleton charted space associated to f is a manifold.

Русский

Если f — открытая вложенность, сопряжённое ей единичное пространство диаграмм образует множество для многообразия.

LaTeX

$$IsManifold I n (h.singletonChartedSpace)$$

Lean4

theorem isManifold_singleton {𝕜 E H : Type*} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E]
    [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {n : WithTop ℕ∞} {M : Type*} [TopologicalSpace M] [Nonempty M]
    {f : M → H} (h : IsOpenEmbedding f) : @IsManifold 𝕜 _ E _ _ H _ I n M _ h.singletonChartedSpace :=
  (h.toOpenPartialHomeomorph f).isManifold_singleton (by simp)

Похожие утверждения