Theorems · Definition · global analysis

tangentCoordChange

{𝕜 : Type u_1} →
  [inst : NontriviallyNormedField 𝕜] →
    {E : Type u_2} →
      [inst_1 : NormedAddCommGroup E] →
        [inst_2 : NormedSpace 𝕜 E] →
          {H : Type u_4} →
            [inst_3 : TopologicalSpace H] →
              (I : ModelWithCorners 𝕜 E H) →
                {M : Type u_6} →
                  [inst_4 : TopologicalSpace M] →
                    [inst_5 : ChartedSpace H M] → [IsManifold I 1 M] → M → M → M → E →L[𝕜] E

In a manifold M, given two preferred charts indexed by x y : M, tangentCoordChange I x y is the family of derivatives of the corresponding change-of-coordinates map. It takes junk values outside the intersection of the sources of the two charts. Note that this definition takes advantage of the fact that tangentBundleCore has the same base sets as the preferred charts of the base manifold.

Defined in

Mathlib.Geometry.Manifold.VectorBundle.Tangent

Cited by

11 results in Mathlib

Foundations

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

Assumes

NontriviallyNormedFieldNormedAddCommGroupNormedSpaceTopologicalSpaceTopologicalSpaceChartedSpaceIsManifold