Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-06-04 17:34 93fb5345

View on Github →

refactor(topology/vector_bundle): split file (#14535) Also:

Rename pullback -> topological_vector_bundle.pullback
Use delta_instance instead of local attribute [reducible]
Change module doc
Remove transitive import

Estimated changes

Modified src/geometry/manifold/tangent_bundle.lean

Renamed src/topology/vector_bundle.lean to src/topology/vector_bundle/basic.lean

deleted theorem inducing_pullback_total_space_embedding

deleted theorem pullback.continuous_lift

deleted theorem pullback.continuous_proj

deleted theorem pullback.continuous_total_space_mk

deleted def pullback_topology

deleted theorem topological_vector_bundle.prod.inducing_diag

deleted theorem topological_vector_bundle.trivialization.base_set_prod

deleted theorem topological_vector_bundle.trivialization.continuous_linear_equiv_at_prod

deleted theorem topological_vector_bundle.trivialization.prod.continuous_inv_fun

deleted theorem topological_vector_bundle.trivialization.prod.continuous_to_fun

deleted def topological_vector_bundle.trivialization.prod.inv_fun'

deleted theorem topological_vector_bundle.trivialization.prod.left_inv

deleted theorem topological_vector_bundle.trivialization.prod.right_inv

deleted def topological_vector_bundle.trivialization.prod.to_fun'

deleted def topological_vector_bundle.trivialization.prod

deleted theorem topological_vector_bundle.trivialization.prod_apply

deleted theorem topological_vector_bundle.trivialization.prod_symm_apply

deleted def topological_vector_bundle.trivialization.pullback

Created src/topology/vector_bundle/prod.lean

added theorem topological_vector_bundle.prod.inducing_diag

added theorem topological_vector_bundle.trivialization.base_set_prod

added theorem topological_vector_bundle.trivialization.continuous_linear_equiv_at_prod

added theorem topological_vector_bundle.trivialization.prod.continuous_inv_fun

added theorem topological_vector_bundle.trivialization.prod.continuous_to_fun

added def topological_vector_bundle.trivialization.prod.inv_fun'

added theorem topological_vector_bundle.trivialization.prod.left_inv

added theorem topological_vector_bundle.trivialization.prod.right_inv

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

Created src/topology/vector_bundle/pullback.lean

added theorem inducing_pullback_total_space_embedding

added theorem pullback.continuous_lift

added theorem pullback.continuous_proj

added theorem pullback.continuous_total_space_mk

added def pullback_topology

added def topological_vector_bundle.trivialization.pullback