Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-06-24 09:57 d9dcf699

View on Github →

feat(topology/topological_fiber_bundle): a new standard construction for topological fiber bundles (#7935) In this PR we implement a new standard construction for topological fiber bundles: namely a structure that permits to define a fiber bundle when trivializations are given as local equivalences but there is not yet a topology on the total space. The total space is hence given a topology in such a way that there is a fiber bundle structure for which the local equivalences are also local homeomorphism and hence local trivializations.

Estimated changes

Modified src/topology/continuous_on.lean

added theorem preimage_nhds_within_coinduced'

added theorem preimage_nhds_within_coinduced

Modified src/topology/topological_fiber_bundle.lean

modified theorem bundle_trivialization.apply_symm_apply'

modified theorem bundle_trivialization.apply_symm_apply

modified theorem bundle_trivialization.coe_coe

modified theorem bundle_trivialization.coe_fst'

modified theorem bundle_trivialization.coe_fst

modified theorem bundle_trivialization.coe_fst_eventually_eq_proj'

modified theorem bundle_trivialization.coe_fst_eventually_eq_proj

modified theorem bundle_trivialization.coe_mk

modified def bundle_trivialization.comp_homeomorph

modified theorem bundle_trivialization.continuous_at_proj

modified theorem bundle_trivialization.map_proj_nhds

added theorem bundle_trivialization.map_target

modified theorem bundle_trivialization.mem_source

modified theorem bundle_trivialization.mem_target

modified theorem bundle_trivialization.mk_proj_snd'

modified theorem bundle_trivialization.mk_proj_snd

modified theorem bundle_trivialization.proj_symm_apply'

modified theorem bundle_trivialization.proj_symm_apply

modified theorem bundle_trivialization.symm_apply_mk_proj

added def bundle_trivialization.to_prebundle_trivialization

added theorem prebundle_trivialization.apply_symm_apply'

added theorem prebundle_trivialization.apply_symm_apply

added theorem prebundle_trivialization.coe_coe

added theorem prebundle_trivialization.coe_fst'

added theorem prebundle_trivialization.coe_fst

added theorem prebundle_trivialization.mem_source

added theorem prebundle_trivialization.mem_target

added theorem prebundle_trivialization.mk_proj_snd'

added theorem prebundle_trivialization.mk_proj_snd

added theorem prebundle_trivialization.preimage_symm_proj_base_set

added theorem prebundle_trivialization.preimage_symm_proj_inter

added theorem prebundle_trivialization.proj_symm_apply'

added theorem prebundle_trivialization.proj_symm_apply

added def prebundle_trivialization.set_symm

added theorem prebundle_trivialization.symm_apply_mk_proj

added structure prebundle_trivialization

added def topological_fiber_prebundle.bundle_trivialization_at

added theorem topological_fiber_prebundle.continuous_proj

added theorem topological_fiber_prebundle.continuous_symm_trivialization_at

added theorem topological_fiber_prebundle.is_open_source_trivialization_at

added theorem topological_fiber_prebundle.is_open_target_trivialization_at_inter

added theorem topological_fiber_prebundle.is_topological_fiber_bundle

added def topological_fiber_prebundle.total_space_topology

added structure topological_fiber_prebundle