Commit 2022-11-09 00:14 433802f7

refactor(topology/vector_bundle/basic): deduplicate trivialization (#17359) Currently, in mathlib, there is a structure topological_vector_bundle.trivialization which extends another structure topological_fibre_bundle.trivialization by a linearity hypothesis. We change this to a single structure trivialization (no namespace), together with a mixin class trivialization.is_linear. This is the first step in the planned vector bundle refactor: it will allow all the data of a vector bundle to be held at the level of fibre bundles, so that there can be a non-"dangerous instance" charted_space instance associated to a vector bundle. The analogous change is made for pretrivialization. The most awkward aspect of this refactor is that one would want the linearity of trivializations associated to a vector bundle to be "automatic", which effectively means that one wants a trivialization.is_linear instance to be found by typeclass inference for trivializations in the trivialization_atlas of a vector bundle. For this to work, the property of belonging to the trivialization atlas also needs to be made into a Prop typeclass. We call this typeclass mem_trivialization_atlas.