Theorems · Definition · global analysis

VectorField.mpullback

{𝕜 : Type u_1} →
  [inst : NontriviallyNormedField 𝕜] →
    {H : Type u_2} →
      [inst_1 : TopologicalSpace H] →
        {E : Type u_3} →
          [inst_2 : NormedAddCommGroup E] →
            [inst_3 : NormedSpace 𝕜 E] →
              (I : ModelWithCorners 𝕜 E H) →
                {M : Type u_4} →
                  [inst_4 : TopologicalSpace M] →
                    [inst_5 : ChartedSpace H M] →
                      {H' : Type u_5} →
                        [inst_6 : TopologicalSpace H'] →
                          {E' : Type u_6} →
                            [inst_7 : NormedAddCommGroup E'] →
                              [inst_8 : NormedSpace 𝕜 E'] →
                                (I' : ModelWithCorners 𝕜 E' H') →
                                  {M' : Type u_7} →
                                    [inst_9 : TopologicalSpace M'] →
                                      [inst_10 : ChartedSpace H' M'] →
                                        (M → M') → ((x : M') → TangentSpace I' x) → (x : M) → TangentSpace I x

The pullback of a vector field under a map between manifolds. If the derivative of the map is not invertible, then pullback is given the junk value zero.

Defined in

Mathlib.Geometry.Manifold.VectorField.Pullback

Cited by

41 results in Mathlib

Foundations

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

Assumes

NontriviallyNormedFieldTopologicalSpaceNormedAddCommGroupNormedSpaceTopologicalSpaceChartedSpaceTopologicalSpaceNormedAddCommGroupNormedSpaceTopologicalSpaceChartedSpace