Theorems · Definition · global analysis

Bundle.Trivialization.localFrame

{𝕜 : 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} →
                              (e : Bundle.Trivialization F Bundle.TotalSpace.proj) →
                                [MemTrivializationAtlas e] → Module.Basis ι 𝕜 F → ι → (x : M) → V x

The local frame on V induced by a compatible local trivialization e of V and a basis b of the model fiber F. Use e.localFrame b i to access the i-th section in that frame. If x is outside of e.baseSet, this returns the junk value 0.

Defined in

Mathlib.Geometry.Manifold.VectorBundle.LocalFrame

Cited by

11 results in Mathlib

Foundations

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

Assumes

NontriviallyNormedFieldTopologicalSpaceNormedAddCommGroupNormedSpaceTopologicalSpaceAddCommGroupModuleTopologicalSpaceFiberBundleVectorBundleMemTrivializationAtlas