Theorems · Definition · global analysis

contDiffGroupoid

WithTop ℕ∞ →
  {𝕜 : 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 → StructureGroupoid H

Given a model with corners (E, H), we define the groupoid of invertible C^n transformations of H as the invertible maps that are C^n when read in E through I.

Defined in

Mathlib.Geometry.Manifold.IsManifold.Basic

Cited by

28 results in Mathlib

Foundations

Depth 202 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

NontriviallyNormedFieldNormedAddCommGroupNormedSpaceTopologicalSpace