Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-03-08 17:53 feb24fb6

View on Github →

feat(topology/vector_bundle): direct sum of topological vector bundles (#12512)

Estimated changes

Modified src/data/bundle.lean

Modified src/topology/maps.lean

Modified src/topology/vector_bundle.lean

added theorem topological_vector_bundle.continuous_proj

added theorem topological_vector_bundle.prod.inducing_diag

added theorem topological_vector_bundle.trivialization.apply_eq_prod_continuous_linear_equiv_at

added theorem topological_vector_bundle.trivialization.base_set_prod

added theorem topological_vector_bundle.trivialization.continuous_linear_equiv_at_prod

added def topological_vector_bundle.trivialization.prod.inv_fun'

added theorem topological_vector_bundle.trivialization.prod.inv_fun'_apply

added def topological_vector_bundle.trivialization.prod.to_fun'

added def topological_vector_bundle.trivialization.prod

added theorem topological_vector_bundle.trivialization.prod_apply

added theorem topological_vector_bundle.trivialization.prod_symm_apply

added theorem topological_vector_bundle.trivialization.symm_apply_eq_mk_continuous_linear_equiv_at_symm