mk' — Mathlib

English

Compatibility of atlas implies IsManifold given a HasGroupoid instance.

Русский

Совместимость атласа гарантирует IsManifold из экземпляра HasGroupoid.

LaTeX

$$$IsManifold I n M$ provided by $gr : HasGroupoid M (contDiffGroupoid n I)$$$

Lean4

/-- Building a `C^n` manifold from a `HasGroupoid` assumption. -/
theorem mk' {𝕜 : Type*} [NontriviallyNormedField 𝕜] {E : Type*} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type*}
    [TopologicalSpace H] (I : ModelWithCorners 𝕜 E H) (n : WithTop ℕ∞) (M : Type*) [TopologicalSpace M]
    [ChartedSpace H M] [gr : HasGroupoid M (contDiffGroupoid n I)] : IsManifold I n M :=
  { gr with }

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