Mathlib v3 is deprecated. Go to Mathlib v4

Theorem topological_vector_bundle.trivialization.prod.inv_fun'_apply

Modification history

2022-05-25 09:48
src/topology/vector_bundle.lean
feat(topology/vector_bundle): use trivialization.symm to simplify the product of vector bundles (#14361)
Deleted topological_vector_bundle.trivialization.prod.inv_fun'_applyView on Github →
2022-03-08 17:53
src/topology/vector_bundle.lean
feat(topology/vector_bundle): direct sum of topological vector bundles (#12512)
Added topological_vector_bundle.trivialization.prod.inv_fun'_applyView on Github →