Theorems · Definition · global analysis

TangentSpace

{𝕜 : Type u_1} →
  [inst : NontriviallyNormedField 𝕜] →
    {E : Type u} →
      [inst_1 : NormedAddCommGroup E] →
        [inst_2 : NormedSpace 𝕜 E] →
          {H : Type u_2} →
            [inst_3 : TopologicalSpace H] →
              ModelWithCorners 𝕜 E H → {M : Type u_3} → [inst : TopologicalSpace M] → [ChartedSpace H M] → M → Type u

The tangent space at a point of the manifold M. It is just E. We could use instead (tangentBundleCore I M).toFiberBundleCore.fiber x, but we use E to help the kernel. The definition of TangentSpace is not reducible so that type class inference does not pick wrong instances.

Defined in

Mathlib.Geometry.Manifold.IsManifold.Basic

Cited by

555 results in Mathlib

Foundations

Depth 12 from the axioms, rests on 72 definitions · uses no axioms

Assumes

NontriviallyNormedFieldNormedAddCommGroupNormedSpaceTopologicalSpaceTopologicalSpaceChartedSpace