isManifold_singleton — Mathlib

English

The singleton charted space coming from an open partial homeomorphism e with source equal to the whole space M is a manifold.

Русский

Одиночное пространство диаграмм, полученное из частичной открытой гомоморфизмы e при source = всё M, является многообразием.

LaTeX

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

Lean4

theorem isManifold_singleton {𝕜 : Type*} [NontriviallyNormedField 𝕜] {E : Type*} [NormedAddCommGroup E]
    [NormedSpace 𝕜 E] {H : Type*} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {n : WithTop ℕ∞} {M : Type*}
    [TopologicalSpace M] (e : OpenPartialHomeomorph M H) (h : e.source = Set.univ) :
    @IsManifold 𝕜 _ E _ _ H _ I n M _ (e.singletonChartedSpace h) :=
  @IsManifold.mk' _ _ _ _ _ _ _ _ _ _ _ (id _) <| e.singleton_hasGroupoid h (contDiffGroupoid n I)

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