Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2023-07-02 14:35 e473c319

View on Github →

refactor: redefine bundle.total_space (#19221)

Use a custom structure for bundle.total_space.
- Use bundle.total_space.mk instead of bundle.total_space_mk.
- Use bundle.total_space.to_prod instead of equiv.sigma_equiv_prod.
- Use bundle.total_space.mk' (scoped notation) to specify F.
- Rename bundle.trivial.proj_snd to bundle.total_space.trivial_snd to allow dot notation. Should we just use bundle.total_space.snd since bundle.trivial is now reducible?
Add an unused argument to bundle.total_space.
Make bundle.trivial and bundle.continuous_linear_map reducible.
Drop instances that are no longer needed.

Estimated changes

Modified src/data/bundle.lean

deleted theorem bundle.coe_fst

deleted theorem bundle.coe_snd

modified theorem bundle.coe_snd_map_apply

modified theorem bundle.coe_snd_map_smul

modified def bundle.pullback.lift

modified theorem bundle.pullback.lift_mk

deleted theorem bundle.pullback.proj_lift

modified def bundle.pullback

deleted theorem bundle.pullback_total_space_embedding_snd

deleted theorem bundle.sigma_mk_eq_total_space_mk

deleted theorem bundle.to_total_space_coe

added theorem bundle.total_space.coe_eq_mk

added theorem bundle.total_space.coe_proj

added theorem bundle.total_space.coe_snd

modified theorem bundle.total_space.eta

deleted def bundle.total_space.proj

deleted theorem bundle.total_space.proj_mk

added def bundle.total_space.to_prod

added def bundle.total_space.trivial_snd

added structure bundle.total_space

deleted def bundle.total_space

deleted def bundle.total_space_mk

deleted def bundle.trivial.proj_snd

modified def bundle.trivial

Modified src/geometry/manifold/cont_mdiff_mfderiv.lean

Modified src/geometry/manifold/mfderiv.lean

deleted theorem tangent_map_fst

deleted theorem tangent_map_within_fst

Modified src/geometry/manifold/vector_bundle/basic.lean

modified theorem bundle.cont_mdiff_at_proj

modified theorem bundle.cont_mdiff_at_total_space

modified theorem bundle.cont_mdiff_on_proj

modified theorem bundle.cont_mdiff_proj

modified theorem bundle.cont_mdiff_within_at_total_space

modified theorem bundle.smooth_at_proj

modified theorem bundle.smooth_on_proj

modified theorem bundle.smooth_proj

modified theorem bundle.smooth_zero_section

modified theorem fiber_bundle.charted_space_chart_at

modified theorem fiber_bundle.charted_space_chart_at_symm_fst

Modified src/geometry/manifold/vector_bundle/hom.lean

Modified src/geometry/manifold/vector_bundle/pullback.lean

Modified src/geometry/manifold/vector_bundle/smooth_section.lean

Modified src/geometry/manifold/vector_bundle/tangent.lean

modified def tangent_bundle

Modified src/topology/covering.lean

Modified src/topology/fiber_bundle/basic.lean

modified theorem fiber_bundle.continuous_at_total_space

modified theorem fiber_bundle.continuous_proj

modified theorem fiber_bundle.continuous_total_space_mk

modified theorem fiber_bundle.continuous_within_at_total_space

modified theorem fiber_bundle.is_open_map_proj

modified theorem fiber_bundle.map_proj_nhds

modified theorem fiber_bundle.mem_trivialization_at_proj_source

modified theorem fiber_bundle.quotient_map_proj

modified theorem fiber_bundle.surjective_proj

modified theorem fiber_bundle.trivialization_at_proj_fst

modified def fiber_bundle_core.local_triv_at

modified def fiber_bundle_core.total_space

modified theorem fiber_prebundle.continuous_on_of_comp_right

modified theorem fiber_prebundle.continuous_proj

modified theorem fiber_prebundle.is_open_source

modified theorem fiber_prebundle.is_open_target_of_mem_pretrivialization_atlas_inter

modified def fiber_prebundle.total_space_topology

Modified src/topology/fiber_bundle/constructions.lean

modified theorem bundle.trivial.eq_trivialization

modified def bundle.trivial.trivialization

modified theorem pullback.continuous_lift

modified theorem pullback.continuous_proj

modified def pullback_topology

modified theorem trivialization.prod.continuous_to_fun

modified theorem trivialization.prod.left_inv

modified def trivialization.prod.to_fun'

modified theorem trivialization.prod_symm_apply

Modified src/topology/fiber_bundle/trivialization.lean

modified theorem pretrivialization.apply_mk_symm

modified theorem pretrivialization.coe_mem_source

modified theorem pretrivialization.coe_symm_of_not_mem

modified theorem pretrivialization.mk_symm

modified theorem pretrivialization.symm_apply

modified theorem pretrivialization.symm_apply_apply_mk

modified theorem pretrivialization.symm_apply_of_not_mem

modified theorem pretrivialization.symm_coe_proj

modified theorem pretrivialization.symm_proj_apply

modified theorem trivialization.apply_mk_symm

modified theorem trivialization.continuous_on_symm

modified theorem trivialization.mk_symm

modified theorem trivialization.symm_apply

modified theorem trivialization.symm_apply_apply

modified theorem trivialization.symm_apply_apply_mk

modified theorem trivialization.symm_apply_of_not_mem

modified theorem trivialization.symm_proj_apply

Modified src/topology/vector_bundle/basic.lean

modified def bundle.zero_section

modified theorem bundle.zero_section_proj

modified theorem bundle.zero_section_snd

modified theorem continuous_on_coord_change

modified theorem pretrivialization.coe_linear_map_at

modified theorem pretrivialization.coe_linear_map_at_of_mem

modified def pretrivialization.linear_equiv_at

modified theorem pretrivialization.linear_map_at_apply

modified theorem pretrivialization.linear_map_at_def_of_mem

modified theorem pretrivialization.linear_map_at_def_of_not_mem

modified theorem pretrivialization.linear_map_at_eq_zero

modified theorem pretrivialization.linear_map_at_symmₗ

modified theorem pretrivialization.symmₗ_linear_map_at

modified theorem trivialization.apply_eq_prod_continuous_linear_equiv_at

modified theorem trivialization.apply_symm_apply_eq_coord_changeL

modified theorem trivialization.coe_continuous_linear_equiv_at_eq

modified theorem trivialization.coe_coord_changeL'

modified theorem trivialization.coe_coord_changeL

modified theorem trivialization.coe_linear_map_at

modified theorem trivialization.coe_linear_map_at_of_mem

modified theorem trivialization.coe_symmₗ

modified theorem trivialization.comp_continuous_linear_equiv_at_eq_coord_change

modified def trivialization.continuous_linear_equiv_at

modified theorem trivialization.continuous_linear_equiv_at_apply'

modified def trivialization.continuous_linear_map_at

modified theorem trivialization.continuous_linear_map_at_symmL

modified def trivialization.coord_changeL

modified theorem trivialization.coord_changeL_apply'

modified theorem trivialization.coord_changeL_apply

modified theorem trivialization.coord_changeL_symm_apply

modified def trivialization.linear_equiv_at

modified theorem trivialization.linear_equiv_at_apply

modified theorem trivialization.linear_equiv_at_symm_apply

modified theorem trivialization.linear_map_at_apply

modified theorem trivialization.linear_map_at_def_of_mem

modified theorem trivialization.linear_map_at_def_of_not_mem

modified theorem trivialization.linear_map_at_symmₗ

modified theorem trivialization.mk_coord_changeL

modified def trivialization.symmL

modified theorem trivialization.symmL_continuous_linear_map_at

modified theorem trivialization.symm_apply_eq_mk_continuous_linear_equiv_at_symm

modified theorem trivialization.symm_continuous_linear_equiv_at_eq

modified theorem trivialization.symm_coord_changeL

modified theorem trivialization.symmₗ_linear_map_at

modified def vector_bundle_core.local_triv

modified def vector_bundle_core.local_triv_at

Modified src/topology/vector_bundle/constructions.lean

modified theorem trivialization.continuous_linear_equiv_at_prod

Modified src/topology/vector_bundle/hom.lean