Documentation

Mathlib.Geometry.Manifold.VectorBundle.Tangent

Tangent bundles #

This file defines the tangent bundle as a smooth vector bundle.

Let M be a smooth manifold with corners with model I on (E, H). We define the tangent bundle of M using the VectorBundleCore construction indexed by the charts of M with fibers E. Given two charts i, j : LocalHomeomorph M H, the coordinate change between i and j at a point x : M is the derivative of the composite

  I.symm   i.symm    j     I
E -----> H -----> M --> H --> E

within the set range I โŠ† E at I (i x) : E. This defines a smooth vector bundle TangentBundle with fibers TangentSpace.

Main definitions #

theorem contDiffOn_fderiv_coord_change {๐•œ : Type u_1} [NontriviallyNormedField ๐•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ๐•œ E] {H : Type u_4} [TopologicalSpace H] (I : ModelWithCorners ๐•œ E H) {M : Type u_6} [TopologicalSpace M] [ChartedSpace H M] [SmoothManifoldWithCorners I M] (i : โ†‘(atlas H M)) (j : โ†‘(atlas H M)) :
ContDiffOn ๐•œ โŠค (fderivWithin ๐•œ (โ†‘(LocalHomeomorph.extend (โ†‘j) I) โˆ˜ โ†‘(LocalEquiv.symm (LocalHomeomorph.extend (โ†‘i) I))) (Set.range โ†‘I)) (LocalEquiv.trans (LocalEquiv.symm (LocalHomeomorph.extend (โ†‘i) I)) (LocalHomeomorph.extend (โ†‘j) I)).source

Auxiliary lemma for tangent spaces: the derivative of a coordinate change between two charts is smooth on its source.

@[simp]
theorem tangentBundleCore_indexAt {๐•œ : Type u_1} [NontriviallyNormedField ๐•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ๐•œ E] {H : Type u_4} [TopologicalSpace H] (I : ModelWithCorners ๐•œ E H) (M : Type u_6) [TopologicalSpace M] [ChartedSpace H M] [SmoothManifoldWithCorners I M] (x : M) :
@[simp]
theorem tangentBundleCore_coordChange {๐•œ : Type u_1} [NontriviallyNormedField ๐•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ๐•œ E] {H : Type u_4} [TopologicalSpace H] (I : ModelWithCorners ๐•œ E H) (M : Type u_6) [TopologicalSpace M] [ChartedSpace H M] [SmoothManifoldWithCorners I M] (i : โ†‘(atlas H M)) (j : โ†‘(atlas H M)) (x : M) :
VectorBundleCore.coordChange (tangentBundleCore I M) i j x = fderivWithin ๐•œ (โ†‘(LocalHomeomorph.extend (โ†‘j) I) โˆ˜ โ†‘(LocalEquiv.symm (LocalHomeomorph.extend (โ†‘i) I))) (Set.range โ†‘I) (โ†‘(LocalHomeomorph.extend (โ†‘i) I) x)
def tangentBundleCore {๐•œ : Type u_1} [NontriviallyNormedField ๐•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ๐•œ E] {H : Type u_4} [TopologicalSpace H] (I : ModelWithCorners ๐•œ E H) (M : Type u_6) [TopologicalSpace M] [ChartedSpace H M] [SmoothManifoldWithCorners I M] :
VectorBundleCore ๐•œ M E โ†‘(atlas H M)

Let M be a smooth manifold with corners with model I on (E, H). Then VectorBundleCore I M is the vector bundle core for the tangent bundle over M. It is indexed by the atlas of M, with fiber E and its change of coordinates from the chart i to the chart j at point x : M is the derivative of the composite

  I.symm   i.symm    j     I
E -----> H -----> M --> H --> E

within the set range I โŠ† E at I (i x) : E.

Instances For
    @[simp]
    theorem tangentBundleCore_baseSet {๐•œ : Type u_1} [NontriviallyNormedField ๐•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ๐•œ E] {H : Type u_4} [TopologicalSpace H] (I : ModelWithCorners ๐•œ E H) (M : Type u_6) [TopologicalSpace M] [ChartedSpace H M] [SmoothManifoldWithCorners I M] (i : โ†‘(atlas H M)) :
    VectorBundleCore.baseSet (tangentBundleCore I M) i = (โ†‘i).source
    theorem tangentBundleCore_coordChange_achart {๐•œ : Type u_1} [NontriviallyNormedField ๐•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ๐•œ E] {H : Type u_4} [TopologicalSpace H] (I : ModelWithCorners ๐•œ E H) {M : Type u_6} [TopologicalSpace M] [ChartedSpace H M] [SmoothManifoldWithCorners I M] (x : M) (x' : M) (z : M) :
    VectorBundleCore.coordChange (tangentBundleCore I M) (achart H x) (achart H x') z = fderivWithin ๐•œ (โ†‘(extChartAt I x') โˆ˜ โ†‘(LocalEquiv.symm (extChartAt I x))) (Set.range โ†‘I) (โ†‘(extChartAt I x) z)
    def TangentSpace {๐•œ : Type u_10} [NontriviallyNormedField ๐•œ] {E : Type u_9} [NormedAddCommGroup E] [NormedSpace ๐•œ E] {H : Type u_11} [TopologicalSpace H] (I : ModelWithCorners ๐•œ E H) {M : Type u_12} [TopologicalSpace M] [ChartedSpace H M] [SmoothManifoldWithCorners I M] (_x : M) :
    Type u_9

    The tangent space at a point of the manifold M. It is just E. We could use instead (tangentBundleCore I M).to_topological_vector_bundle_core.fiber x, but we use E to help the kernel.

    Instances For
      instance instTopologicalSpaceTangentSpace {๐•œ : Type u_1} [NontriviallyNormedField ๐•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ๐•œ E] {H : Type u_4} [TopologicalSpace H] (I : ModelWithCorners ๐•œ E H) {M : Type u_6} [TopologicalSpace M] [ChartedSpace H M] [SmoothManifoldWithCorners I M] {x : M} :
      instance instAddCommGroupTangentSpace {๐•œ : Type u_1} [NontriviallyNormedField ๐•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ๐•œ E] {H : Type u_4} [TopologicalSpace H] (I : ModelWithCorners ๐•œ E H) {M : Type u_6} [TopologicalSpace M] [ChartedSpace H M] [SmoothManifoldWithCorners I M] {x : M} :
      @[reducible]
      def TangentBundle {๐•œ : Type u_1} [NontriviallyNormedField ๐•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ๐•œ E] {H : Type u_4} [TopologicalSpace H] (I : ModelWithCorners ๐•œ E H) (M : Type u_6) [TopologicalSpace M] [ChartedSpace H M] [SmoothManifoldWithCorners I M] :
      Type (max u_6 u_2)

      The tangent bundle to a smooth manifold, as a Sigma type. Defined in terms of Bundle.TotalSpace to be able to put a suitable topology on it.

      Instances For
        instance instInhabitedTangentSpace {๐•œ : Type u_1} [NontriviallyNormedField ๐•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ๐•œ E] {H : Type u_4} [TopologicalSpace H] (I : ModelWithCorners ๐•œ E H) {M : Type u_6} [TopologicalSpace M] [ChartedSpace H M] [SmoothManifoldWithCorners I M] (x : M) :
        instance instTopologicalSpaceTangentBundle {๐•œ : Type u_1} [NontriviallyNormedField ๐•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ๐•œ E] {H : Type u_4} [TopologicalSpace H] (I : ModelWithCorners ๐•œ E H) (M : Type u_6) [TopologicalSpace M] [ChartedSpace H M] [SmoothManifoldWithCorners I M] :
        instance TangentSpace.fiberBundle {๐•œ : Type u_1} [NontriviallyNormedField ๐•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ๐•œ E] {H : Type u_4} [TopologicalSpace H] (I : ModelWithCorners ๐•œ E H) (M : Type u_6) [TopologicalSpace M] [ChartedSpace H M] [SmoothManifoldWithCorners I M] :
        instance TangentSpace.vectorBundle {๐•œ : Type u_1} [NontriviallyNormedField ๐•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ๐•œ E] {H : Type u_4} [TopologicalSpace H] (I : ModelWithCorners ๐•œ E H) (M : Type u_6) [TopologicalSpace M] [ChartedSpace H M] [SmoothManifoldWithCorners I M] :
        VectorBundle ๐•œ E (TangentSpace I)
        @[simp]
        theorem TangentBundle.trivializationAt_source {๐•œ : Type u_1} [NontriviallyNormedField ๐•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ๐•œ E] {H : Type u_4} [TopologicalSpace H] (I : ModelWithCorners ๐•œ E H) (M : Type u_6) [TopologicalSpace M] [ChartedSpace H M] [SmoothManifoldWithCorners I M] (x : M) :
        (trivializationAt E (TangentSpace I) x).toLocalHomeomorph.toLocalEquiv.source = Bundle.TotalSpace.proj โปยน' (chartAt H x).toLocalEquiv.source
        @[simp]
        theorem TangentBundle.trivializationAt_target {๐•œ : Type u_1} [NontriviallyNormedField ๐•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ๐•œ E] {H : Type u_4} [TopologicalSpace H] (I : ModelWithCorners ๐•œ E H) (M : Type u_6) [TopologicalSpace M] [ChartedSpace H M] [SmoothManifoldWithCorners I M] (x : M) :
        (trivializationAt E (TangentSpace I) x).toLocalHomeomorph.toLocalEquiv.target = (chartAt H x).toLocalEquiv.source ร—หข Set.univ
        @[simp]
        theorem TangentBundle.trivializationAt_baseSet {๐•œ : Type u_1} [NontriviallyNormedField ๐•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ๐•œ E] {H : Type u_4} [TopologicalSpace H] (I : ModelWithCorners ๐•œ E H) (M : Type u_6) [TopologicalSpace M] [ChartedSpace H M] [SmoothManifoldWithCorners I M] (x : M) :
        (trivializationAt E (TangentSpace I) x).baseSet = (chartAt H x).toLocalEquiv.source
        theorem TangentBundle.trivializationAt_apply {๐•œ : Type u_1} [NontriviallyNormedField ๐•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ๐•œ E] {H : Type u_4} [TopologicalSpace H] (I : ModelWithCorners ๐•œ E H) (M : Type u_6) [TopologicalSpace M] [ChartedSpace H M] [SmoothManifoldWithCorners I M] (x : M) (z : TangentBundle I M) :
        โ†‘(trivializationAt E (TangentSpace I) x) z = (z.proj, โ†‘(fderivWithin ๐•œ (โ†‘(LocalHomeomorph.extend (chartAt H x) I) โˆ˜ โ†‘(LocalEquiv.symm (LocalHomeomorph.extend (chartAt H z.proj) I))) (Set.range โ†‘I) (โ†‘(LocalHomeomorph.extend (chartAt H z.proj) I) z.proj)) z.snd)
        @[simp]
        theorem TangentBundle.trivializationAt_fst {๐•œ : Type u_1} [NontriviallyNormedField ๐•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ๐•œ E] {H : Type u_4} [TopologicalSpace H] (I : ModelWithCorners ๐•œ E H) (M : Type u_6) [TopologicalSpace M] [ChartedSpace H M] [SmoothManifoldWithCorners I M] (x : M) (z : TangentBundle I M) :
        (โ†‘(trivializationAt E (TangentSpace I) x) z).fst = z.proj
        @[simp]
        theorem TangentBundle.mem_chart_source_iff {๐•œ : Type u_1} [NontriviallyNormedField ๐•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ๐•œ E] {H : Type u_4} [TopologicalSpace H] (I : ModelWithCorners ๐•œ E H) (M : Type u_6) [TopologicalSpace M] [ChartedSpace H M] [SmoothManifoldWithCorners I M] (p : TangentBundle I M) (q : TangentBundle I M) :
        p โˆˆ (chartAt (ModelProd H E) q).toLocalEquiv.source โ†” p.proj โˆˆ (chartAt H q.proj).toLocalEquiv.source
        @[simp]
        theorem TangentBundle.mem_chart_target_iff {๐•œ : Type u_1} [NontriviallyNormedField ๐•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ๐•œ E] {H : Type u_4} [TopologicalSpace H] (I : ModelWithCorners ๐•œ E H) (M : Type u_6) [TopologicalSpace M] [ChartedSpace H M] [SmoothManifoldWithCorners I M] (p : H ร— E) (q : TangentBundle I M) :
        p โˆˆ (chartAt (ModelProd H E) q).toLocalEquiv.target โ†” p.fst โˆˆ (chartAt H q.proj).toLocalEquiv.target
        @[simp]
        theorem TangentBundle.coe_chartAt_fst {๐•œ : Type u_1} [NontriviallyNormedField ๐•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ๐•œ E] {H : Type u_4} [TopologicalSpace H] (I : ModelWithCorners ๐•œ E H) (M : Type u_6) [TopologicalSpace M] [ChartedSpace H M] [SmoothManifoldWithCorners I M] (p : TangentBundle I M) (q : TangentBundle I M) :
        (โ†‘(chartAt (ModelProd H E) q) p).fst = โ†‘(chartAt H q.proj) p.proj
        @[simp]
        theorem TangentBundle.coe_chartAt_symm_fst {๐•œ : Type u_1} [NontriviallyNormedField ๐•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ๐•œ E] {H : Type u_4} [TopologicalSpace H] (I : ModelWithCorners ๐•œ E H) (M : Type u_6) [TopologicalSpace M] [ChartedSpace H M] [SmoothManifoldWithCorners I M] (p : H ร— E) (q : TangentBundle I M) :
        (โ†‘(LocalHomeomorph.symm (chartAt (ModelProd H E) q)) p).proj = โ†‘(LocalHomeomorph.symm (chartAt H q.proj)) p.fst
        @[simp]
        theorem TangentBundle.trivializationAt_continuousLinearMapAt {๐•œ : Type u_1} [NontriviallyNormedField ๐•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ๐•œ E] {H : Type u_4} [TopologicalSpace H] (I : ModelWithCorners ๐•œ E H) (M : Type u_6) [TopologicalSpace M] [ChartedSpace H M] [SmoothManifoldWithCorners I M] {bโ‚€ : M} {b : M} (hb : b โˆˆ (trivializationAt E (TangentSpace I) bโ‚€).baseSet) :
        @[simp]
        theorem TangentBundle.trivializationAt_symmL {๐•œ : Type u_1} [NontriviallyNormedField ๐•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ๐•œ E] {H : Type u_4} [TopologicalSpace H] (I : ModelWithCorners ๐•œ E H) (M : Type u_6) [TopologicalSpace M] [ChartedSpace H M] [SmoothManifoldWithCorners I M] {bโ‚€ : M} {b : M} (hb : b โˆˆ (trivializationAt E (TangentSpace I) bโ‚€).baseSet) :
        @[simp]
        theorem TangentBundle.coordChange_model_space {๐•œ : Type u_1} [NontriviallyNormedField ๐•œ] {F : Type u_8} [NormedAddCommGroup F] [NormedSpace ๐•œ F] (b : F) (b' : F) (x : F) :
        @[simp]
        theorem TangentBundle.symmL_model_space {๐•œ : Type u_1} [NontriviallyNormedField ๐•œ] {F : Type u_8} [NormedAddCommGroup F] [NormedSpace ๐•œ F] (b : F) (b' : F) :
        @[simp]
        theorem TangentBundle.continuousLinearMapAt_model_space {๐•œ : Type u_1} [NontriviallyNormedField ๐•œ] {F : Type u_8} [NormedAddCommGroup F] [NormedSpace ๐•œ F] (b : F) (b' : F) :
        instance TangentBundle.smoothVectorBundle {๐•œ : Type u_1} [NontriviallyNormedField ๐•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ๐•œ E] {H : Type u_4} [TopologicalSpace H] (I : ModelWithCorners ๐•œ E H) (M : Type u_6) [TopologicalSpace M] [ChartedSpace H M] [SmoothManifoldWithCorners I M] :

        The tangent bundle to the model space #

        @[simp]
        theorem tangentBundle_model_space_chartAt {๐•œ : Type u_1} [NontriviallyNormedField ๐•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ๐•œ E] {H : Type u_4} [TopologicalSpace H] (I : ModelWithCorners ๐•œ E H) (p : TangentBundle I H) :

        In the tangent bundle to the model space, the charts are just the canonical identification between a product type and a sigma type, a.k.a. TotalSpace.toProd.

        @[simp]
        theorem tangentBundle_model_space_coe_chartAt {๐•œ : Type u_1} [NontriviallyNormedField ๐•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ๐•œ E] {H : Type u_4} [TopologicalSpace H] (I : ModelWithCorners ๐•œ E H) (p : TangentBundle I H) :
        โ†‘(chartAt (ModelProd H E) p) = โ†‘(Bundle.TotalSpace.toProd H E)
        @[simp]
        theorem tangentBundle_model_space_coe_chartAt_symm {๐•œ : Type u_1} [NontriviallyNormedField ๐•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ๐•œ E] {H : Type u_4} [TopologicalSpace H] (I : ModelWithCorners ๐•œ E H) (p : TangentBundle I H) :
        โ†‘(LocalHomeomorph.symm (chartAt (ModelProd H E) p)) = โ†‘(Bundle.TotalSpace.toProd H E).symm
        theorem tangentBundleCore_coordChange_model_space {๐•œ : Type u_1} [NontriviallyNormedField ๐•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ๐•œ E] {H : Type u_4} [TopologicalSpace H] (I : ModelWithCorners ๐•œ E H) (x : H) (x' : H) (z : H) :
        def tangentBundleModelSpaceHomeomorph {๐•œ : Type u_1} [NontriviallyNormedField ๐•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ๐•œ E] (H : Type u_4) [TopologicalSpace H] (I : ModelWithCorners ๐•œ E H) :

        The canonical identification between the tangent bundle to the model space and the product, as a homeomorphism

        Instances For
          @[simp]
          theorem tangentBundleModelSpaceHomeomorph_coe {๐•œ : Type u_1} [NontriviallyNormedField ๐•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ๐•œ E] (H : Type u_4) [TopologicalSpace H] (I : ModelWithCorners ๐•œ E H) :
          @[simp]
          theorem tangentBundleModelSpaceHomeomorph_coe_symm {๐•œ : Type u_1} [NontriviallyNormedField ๐•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ๐•œ E] (H : Type u_4) [TopologicalSpace H] (I : ModelWithCorners ๐•œ E H) :
          theorem inCoordinates_tangent_bundle_core_model_space {๐•œ : Type u_1} [NontriviallyNormedField ๐•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ๐•œ E] {E' : Type u_3} [NormedAddCommGroup E'] [NormedSpace ๐•œ E'] {H : Type u_4} [TopologicalSpace H] (I : ModelWithCorners ๐•œ E H) {H' : Type u_5} [TopologicalSpace H'] (I' : ModelWithCorners ๐•œ E' H') (xโ‚€ : H) (x : H) (yโ‚€ : H') (y : H') (ฯ• : E โ†’L[๐•œ] E') :
          ContinuousLinearMap.inCoordinates E (TangentSpace I) E' (TangentSpace I') xโ‚€ x yโ‚€ y ฯ• = ฯ•

          The map in_coordinates for the tangent bundle is trivial on the model spaces

          def inTangentCoordinates {๐•œ : Type u_1} [NontriviallyNormedField ๐•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ๐•œ E] {E' : Type u_3} [NormedAddCommGroup E'] [NormedSpace ๐•œ E'] {H : Type u_4} [TopologicalSpace H] (I : ModelWithCorners ๐•œ E H) {H' : Type u_5} [TopologicalSpace H'] (I' : ModelWithCorners ๐•œ E' H') {M : Type u_6} [TopologicalSpace M] [ChartedSpace H M] [SmoothManifoldWithCorners I M] {M' : Type u_7} [TopologicalSpace M'] [ChartedSpace H' M'] [SmoothManifoldWithCorners I' M'] {N : Type u_9} (f : N โ†’ M) (g : N โ†’ M') (ฯ• : N โ†’ E โ†’L[๐•œ] E') :
          N โ†’ N โ†’ E โ†’L[๐•œ] E'

          When ฯ• x is a continuous linear map that changes vectors in charts around f x to vectors in charts around g x, inTangentCoordinates I I' f g ฯ• xโ‚€ x is a coordinate change of this continuous linear map that makes sense from charts around f xโ‚€ to charts around g xโ‚€ by composing it with appropriate coordinate changes. Note that the type of ฯ• is more accurately ฮ  x : N, TangentSpace I (f x) โ†’L[๐•œ] TangentSpace I' (g x). We are unfolding TangentSpace in this type so that Lean recognizes that the type of ฯ• doesn't actually depend on f or g.

          This is the underlying function of the trivializations of the hom of (pullbacks of) tangent spaces.

          Instances For
            theorem inTangentCoordinates_model_space {๐•œ : Type u_1} [NontriviallyNormedField ๐•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ๐•œ E] {E' : Type u_3} [NormedAddCommGroup E'] [NormedSpace ๐•œ E'] {H : Type u_4} [TopologicalSpace H] (I : ModelWithCorners ๐•œ E H) {H' : Type u_5} [TopologicalSpace H'] (I' : ModelWithCorners ๐•œ E' H') {N : Type u_9} (f : N โ†’ H) (g : N โ†’ H') (ฯ• : N โ†’ E โ†’L[๐•œ] E') (xโ‚€ : N) :
            inTangentCoordinates I I' f g ฯ• xโ‚€ = ฯ•
            theorem inTangentCoordinates_eq {๐•œ : Type u_1} [NontriviallyNormedField ๐•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ๐•œ E] {E' : Type u_3} [NormedAddCommGroup E'] [NormedSpace ๐•œ E'] {H : Type u_4} [TopologicalSpace H] (I : ModelWithCorners ๐•œ E H) {H' : Type u_5} [TopologicalSpace H'] (I' : ModelWithCorners ๐•œ E' H') {M : Type u_6} [TopologicalSpace M] [ChartedSpace H M] [SmoothManifoldWithCorners I M] {M' : Type u_7} [TopologicalSpace M'] [ChartedSpace H' M'] [SmoothManifoldWithCorners I' M'] {N : Type u_9} (f : N โ†’ M) (g : N โ†’ M') (ฯ• : N โ†’ E โ†’L[๐•œ] E') {xโ‚€ : N} {x : N} (hx : f x โˆˆ (chartAt H (f xโ‚€)).toLocalEquiv.source) (hy : g x โˆˆ (chartAt H' (g xโ‚€)).toLocalEquiv.source) :
            inTangentCoordinates I I' f g ฯ• xโ‚€ x = ContinuousLinearMap.comp (VectorBundleCore.coordChange (tangentBundleCore I' M') (achart H' (g x)) (achart H' (g xโ‚€)) (g x)) (ContinuousLinearMap.comp (ฯ• x) (VectorBundleCore.coordChange (tangentBundleCore I M) (achart H (f xโ‚€)) (achart H (f x)) (f x)))