Theorems · Inductive type · global analysis

IsManifold

{𝕜 : Type u_1} →
  [inst : NontriviallyNormedField 𝕜] →
    {E : Type u_2} →
      [inst_1 : NormedAddCommGroup E] →
        [inst_2 : NormedSpace 𝕜 E] →
          {H : Type u_3} →
            [inst_3 : TopologicalSpace H] →
              ModelWithCorners 𝕜 E H →
                WithTop ℕ∞ → (M : Type u_4) → [inst : TopologicalSpace M] → [ChartedSpace H M] → Prop

Typeclass defining manifolds with respect to a model with corners, over a field 𝕜. This definition includes the model with corners I (which might allow boundary, corners, or not, so this class covers both manifolds with boundary and manifolds without boundary), and a smoothness parameter n : ℕ∞ω (where n = 0 means topological manifold, n = ∞ means smooth manifold and n = ω means analytic manifold).

Defined in

Mathlib.Geometry.Manifold.IsManifold.Basic

Cited by

326 results in Mathlib

Foundations

Depth 12 from the axioms, rests on 75 definitions · uses no axioms

Assumes

NontriviallyNormedFieldNormedAddCommGroupNormedSpaceTopologicalSpaceTopologicalSpaceChartedSpace