mathlib3

433802f7 - refactor(topology/vector_bundle/basic): deduplicate `trivialization` (#17359)

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](https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/Smooth.20vector.20bundles): 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`. Co-authored-by: Floris van Doorn <fpvdoorn@gmail.com>