Theorems · Definition · global analysis

Bundle.Trivialization.basisAt

{𝕜 : Type u_1} →
  [inst : NontriviallyNormedField 𝕜] →
    {M : Type u_4} →
      [inst_1 : TopologicalSpace M] →
        {F : Type u_5} →
          [inst_2 : NormedAddCommGroup F] →
            [inst_3 : NormedSpace 𝕜 F] →
              {V : M → Type u_6} →
                [inst_4 : TopologicalSpace (Bundle.TotalSpace F V)] →
                  [inst_5 : (x : M) → AddCommGroup (V x)] →
                    [inst_6 : (x : M) → Module 𝕜 (V x)] →
                      [inst_7 : (x : M) → TopologicalSpace (V x)] →
                        [inst_8 : FiberBundle F V] →
                          [VectorBundle 𝕜 F V] →
                            {ι : Type u_7} →
                              {x : M} →
                                (e : Bundle.Trivialization F Bundle.TotalSpace.proj) →
                                  [MemTrivializationAtlas e] →
                                    Module.Basis ι 𝕜 F → x ∈ e.baseSet → Module.Basis ι 𝕜 (V x)

Given a compatible local trivialisation e of V and a basis b of the model fiber F, return the corresponding basis of V x.

Defined in

Mathlib.Geometry.Manifold.VectorBundle.LocalFrame

Cited by

5 results in Mathlib

Foundations

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

Assumes

NontriviallyNormedFieldTopologicalSpaceNormedAddCommGroupNormedSpaceTopologicalSpaceAddCommGroupModuleTopologicalSpaceFiberBundleVectorBundleMemTrivializationAtlas