Theorems · Definition · global analysis

PointedContMDiffMap

(𝕜 : 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 →
                (M : Type u_4) →
                  [inst : TopologicalSpace M] → [ChartedSpace H M] → WithTop ℕ∞ → M → Type (max 0 u_4 u_1)

Type synonym, introduced to put a different SMul action on C^n⟮I, M; 𝕜⟯ which is defined as f • r = f(x) * r. Denoted as C^n⟮I, M; 𝕜⟯⟨x⟩ within the Derivation namespace.

Defined in

Mathlib.Geometry.Manifold.DerivationBundle

Cited by

15 results in Mathlib

Foundations

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

Assumes

NontriviallyNormedFieldNormedAddCommGroupNormedSpaceTopologicalSpaceTopologicalSpaceChartedSpace