Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-07-12 22:46 9dfb9a6e

View on Github →

chore(topology/topological_fiber_bundle): renaming (#8270) In this PR I changed

prebundle_trivialization to topological_fiber_bundle.pretrivialization
bundle_trivialization to topological_fiber_bundle.trivialization so to make names consistent with vector_bundle. I also changed the name of the file for consistency.

Estimated changes

Modified src/geometry/manifold/basic_smooth_bundle.lean

Renamed src/topology/topological_fiber_bundle.lean to src/topology/fiber_bundle.lean

deleted theorem bundle_trivialization.apply_symm_apply'

deleted theorem bundle_trivialization.apply_symm_apply

deleted theorem bundle_trivialization.coe_coe

deleted theorem bundle_trivialization.coe_fst'

deleted theorem bundle_trivialization.coe_fst

deleted theorem bundle_trivialization.coe_fst_eventually_eq_proj'

deleted theorem bundle_trivialization.coe_fst_eventually_eq_proj

deleted theorem bundle_trivialization.coe_mk

deleted def bundle_trivialization.comp_homeomorph

deleted theorem bundle_trivialization.continuous_at_proj

deleted theorem bundle_trivialization.continuous_coord_change

deleted def bundle_trivialization.coord_change

deleted theorem bundle_trivialization.coord_change_apply_snd

deleted theorem bundle_trivialization.coord_change_coord_change

deleted def bundle_trivialization.coord_change_homeomorph

deleted theorem bundle_trivialization.coord_change_homeomorph_coe

deleted theorem bundle_trivialization.coord_change_same

deleted theorem bundle_trivialization.coord_change_same_apply

deleted theorem bundle_trivialization.frontier_preimage

deleted theorem bundle_trivialization.is_image_preimage_prod

deleted theorem bundle_trivialization.map_proj_nhds

deleted theorem bundle_trivialization.map_target

deleted theorem bundle_trivialization.mem_source

deleted theorem bundle_trivialization.mem_target

deleted theorem bundle_trivialization.mk_coord_change

deleted theorem bundle_trivialization.mk_proj_snd'

deleted theorem bundle_trivialization.mk_proj_snd

deleted theorem bundle_trivialization.proj_symm_apply'

deleted theorem bundle_trivialization.proj_symm_apply

deleted def bundle_trivialization.restr_open

deleted theorem bundle_trivialization.source_inter_preimage_target_inter

deleted theorem bundle_trivialization.symm_apply_mk_proj

deleted def bundle_trivialization.to_prebundle_trivialization

deleted def bundle_trivialization.trans_fiber_homeomorph

deleted theorem bundle_trivialization.trans_fiber_homeomorph_apply

deleted structure bundle_trivialization

modified theorem is_topological_fiber_bundle.exists_trivialization_Icc_subset

deleted theorem prebundle_trivialization.apply_symm_apply'

deleted theorem prebundle_trivialization.apply_symm_apply

deleted theorem prebundle_trivialization.coe_coe

deleted theorem prebundle_trivialization.coe_fst'

deleted theorem prebundle_trivialization.coe_fst

deleted theorem prebundle_trivialization.mem_source

deleted theorem prebundle_trivialization.mem_target

deleted theorem prebundle_trivialization.mk_proj_snd'

deleted theorem prebundle_trivialization.mk_proj_snd

deleted theorem prebundle_trivialization.preimage_symm_proj_base_set

deleted theorem prebundle_trivialization.preimage_symm_proj_inter

deleted theorem prebundle_trivialization.proj_symm_apply'

deleted theorem prebundle_trivialization.proj_symm_apply

deleted def prebundle_trivialization.set_symm

deleted theorem prebundle_trivialization.symm_apply_mk_proj

deleted structure prebundle_trivialization

added theorem topological_fiber_bundle.pretrivialization.apply_symm_apply'

added theorem topological_fiber_bundle.pretrivialization.apply_symm_apply

added theorem topological_fiber_bundle.pretrivialization.coe_coe

added theorem topological_fiber_bundle.pretrivialization.coe_fst'

added theorem topological_fiber_bundle.pretrivialization.coe_fst

added theorem topological_fiber_bundle.pretrivialization.mem_source

added theorem topological_fiber_bundle.pretrivialization.mem_target

added theorem topological_fiber_bundle.pretrivialization.mk_proj_snd'

added theorem topological_fiber_bundle.pretrivialization.mk_proj_snd

added theorem topological_fiber_bundle.pretrivialization.preimage_symm_proj_base_set

added theorem topological_fiber_bundle.pretrivialization.preimage_symm_proj_inter

added theorem topological_fiber_bundle.pretrivialization.proj_symm_apply'

added theorem topological_fiber_bundle.pretrivialization.proj_symm_apply

added def topological_fiber_bundle.pretrivialization.set_symm

added theorem topological_fiber_bundle.pretrivialization.symm_apply_mk_proj

added structure topological_fiber_bundle.pretrivialization

added theorem topological_fiber_bundle.trivialization.apply_symm_apply'

added theorem topological_fiber_bundle.trivialization.apply_symm_apply

added theorem topological_fiber_bundle.trivialization.coe_coe

added theorem topological_fiber_bundle.trivialization.coe_fst'

added theorem topological_fiber_bundle.trivialization.coe_fst

added theorem topological_fiber_bundle.trivialization.coe_fst_eventually_eq_proj'

added theorem topological_fiber_bundle.trivialization.coe_fst_eventually_eq_proj

added theorem topological_fiber_bundle.trivialization.coe_mk

added def topological_fiber_bundle.trivialization.comp_homeomorph

added theorem topological_fiber_bundle.trivialization.continuous_at_proj

added theorem topological_fiber_bundle.trivialization.continuous_coord_change

added def topological_fiber_bundle.trivialization.coord_change

added theorem topological_fiber_bundle.trivialization.coord_change_apply_snd

added theorem topological_fiber_bundle.trivialization.coord_change_coord_change

added def topological_fiber_bundle.trivialization.coord_change_homeomorph

added theorem topological_fiber_bundle.trivialization.coord_change_homeomorph_coe

added theorem topological_fiber_bundle.trivialization.coord_change_same

added theorem topological_fiber_bundle.trivialization.coord_change_same_apply

added theorem topological_fiber_bundle.trivialization.frontier_preimage

added theorem topological_fiber_bundle.trivialization.is_image_preimage_prod

added theorem topological_fiber_bundle.trivialization.map_proj_nhds

added theorem topological_fiber_bundle.trivialization.map_target

added theorem topological_fiber_bundle.trivialization.mem_source

added theorem topological_fiber_bundle.trivialization.mem_target

added theorem topological_fiber_bundle.trivialization.mk_coord_change

added theorem topological_fiber_bundle.trivialization.mk_proj_snd'

added theorem topological_fiber_bundle.trivialization.mk_proj_snd

added theorem topological_fiber_bundle.trivialization.proj_symm_apply'

added theorem topological_fiber_bundle.trivialization.proj_symm_apply

added def topological_fiber_bundle.trivialization.restr_open

added theorem topological_fiber_bundle.trivialization.source_inter_preimage_target_inter

added theorem topological_fiber_bundle.trivialization.symm_apply_mk_proj

added def topological_fiber_bundle.trivialization.to_pretrivialization

added def topological_fiber_bundle.trivialization.trans_fiber_homeomorph

added theorem topological_fiber_bundle.trivialization.trans_fiber_homeomorph_apply

added structure topological_fiber_bundle.trivialization

modified def topological_fiber_bundle_core.local_triv

modified def topological_fiber_bundle_core.local_triv_at

deleted def topological_fiber_prebundle.bundle_trivialization_at

added theorem topological_fiber_prebundle.continuous_symm_pretrivialization_at

deleted theorem topological_fiber_prebundle.continuous_symm_trivialization_at

added theorem topological_fiber_prebundle.is_open_source_pretrivialization_at

deleted theorem topological_fiber_prebundle.is_open_source_trivialization_at

added theorem topological_fiber_prebundle.is_open_target_pretrivialization_at_inter

deleted theorem topological_fiber_prebundle.is_open_target_trivialization_at_inter

added def topological_fiber_prebundle.trivialization_at

Modified src/topology/vector_bundle.lean

deleted def topological_vector_bundle.trivial_bundle_trivialization

added def topological_vector_bundle.trivial_topological_vector_bundle.trivialization

modified theorem topological_vector_bundle.trivialization.coe_fst

modified def topological_vector_bundle.trivialization.continuous_linear_equiv_at

modified theorem topological_vector_bundle.trivialization.continuous_linear_equiv_at_apply'

modified theorem topological_vector_bundle.trivialization.continuous_linear_equiv_at_apply

modified structure topological_vector_bundle.trivialization