Commit 2022-06-02 15:58 0575db0c

feat(topology/vector_bundle): define some useful linear maps globally (#14484)

• Define pretrivialization.symmₗ, pretrivialization.linear_map_at, trivialization.symmL, trivialization.continuous_linear_map_at
• These are globally-defined (continuous) linear maps. They are linear equivalences on e.base_set, but it is useful to define these globally. They are defined as 0 outside e.base_set
• These are convenient to define the vector bundle of continuous linear maps.