Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-04-14 18:40 f12575e8

View on Github →

feat(topology/topological_fiber_bundle): topological fiber bundle over [a, b] is trivial (#6555)

Estimated changes

Modified src/topology/topological_fiber_bundle.lean

added theorem bundle_trivialization.continuous_coord_change

added def bundle_trivialization.coord_change

added theorem bundle_trivialization.coord_change_apply_snd

added theorem bundle_trivialization.coord_change_coord_change

added def bundle_trivialization.coord_change_homeomorph

added theorem bundle_trivialization.coord_change_homeomorph_coe

added theorem bundle_trivialization.coord_change_same

added theorem bundle_trivialization.coord_change_same_apply

added theorem bundle_trivialization.frontier_preimage

added theorem bundle_trivialization.is_image_preimage_prod

added theorem bundle_trivialization.mk_coord_change

added theorem bundle_trivialization.mk_proj_snd'

added theorem bundle_trivialization.mk_proj_snd

added def bundle_trivialization.restr_open

added def bundle_trivialization.trans_fiber_homeomorph

added theorem bundle_trivialization.trans_fiber_homeomorph_apply

added theorem is_topological_fiber_bundle.exists_trivialization_Icc_subset