mathlib3

8e476fa4 - chore(topology/vector_bundle): use continuous-linear rather than linear in core construction (#13053)

chore(topology/vector_bundle): use continuous-linear rather than linear in core construction (#13053) The `vector_bundle_core` construction builds a vector bundle from a cocycle, the data of which are an open cover and a choice of transition function between any two elements of the cover. Currently, for base `B` and model fibre `F`, the transition function has type `ι → ι → B → (F →ₗ[R] F)`. This PR changes it to type `ι → ι → B → (F →L[R] F)`. This is no loss of generality since there already were other conditions which forced the transition function to be continuous-linear on each fibre. Of course, it is a potential loss of convenience since the proof obligation for continuity now occurs upfront. The change is needed because in the vector bundle refactor to come, the further condition will be imposed that each transition function `B → (F →L[R] F)` is continuous; stating this requires a topology on `F →L[R] F`.