Theorems · Definition · global analysis

ModelWithCorners.tangent

{𝕜 : Type u} →
  [inst : NontriviallyNormedField 𝕜] →
    {E : Type v} →
      [inst_1 : NormedAddCommGroup E] →
        [inst_2 : NormedSpace 𝕜 E] →
          {H : Type w} →
            [inst_3 : TopologicalSpace H] → ModelWithCorners 𝕜 E H → ModelWithCorners 𝕜 (E × E) (ModelProd H E)

Special case of product model with corners, which is trivial on the second factor. This shows up as the model to tangent bundles.

Defined in

Mathlib.Geometry.Manifold.IsManifold.Basic

Cited by

98 results in Mathlib

Foundations

Depth 167 from the axioms, rests on 4,094 definitions · uses propext, Classical.choice, Quot.sound

Assumes

NontriviallyNormedFieldNormedAddCommGroupNormedSpaceTopologicalSpace