Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-05-25 09:48 f8d5c649

View on Github →

feat(topology/vector_bundle): use trivialization.symm to simplify the product of vector bundles (#14361)

Estimated changes

Modified src/topology/vector_bundle.lean

modified def topological_vector_bundle.pretrivialization.linear_equiv_at

modified def topological_vector_bundle.trivialization.continuous_linear_equiv_at

deleted theorem topological_vector_bundle.trivialization.continuous_linear_equiv_at_apply

deleted theorem topological_vector_bundle.trivialization.prod.inv_fun'_apply

modified theorem topological_vector_bundle.trivialization.prod_symm_apply