Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-02-12 12:44 74d3270e

View on Github →

fix(topology/topological_fiber_bundle): fix definition, review (#6184)

fix definition of is_topological_fiber_bundle;
add is_trivial_topological_fiber_bundle;
more lemmas, golf here and there;
define induced fiber bundle.

Estimated changes

Modified src/topology/topological_fiber_bundle.lean

added theorem bundle_trivialization.apply_symm_apply'

added theorem bundle_trivialization.apply_symm_apply

modified theorem bundle_trivialization.coe_coe

added theorem bundle_trivialization.coe_fst'

added theorem bundle_trivialization.coe_fst_eventually_eq_proj'

added theorem bundle_trivialization.coe_fst_eventually_eq_proj

modified theorem bundle_trivialization.coe_mk

added def bundle_trivialization.comp_homeomorph

added theorem bundle_trivialization.map_proj_nhds

added theorem bundle_trivialization.mem_source

added theorem bundle_trivialization.mem_target

added theorem bundle_trivialization.proj_symm_apply'

added theorem bundle_trivialization.proj_symm_apply

added theorem bundle_trivialization.symm_apply_mk_proj

modified structure bundle_trivialization

added theorem is_topological_fiber_bundle.comap

added theorem is_topological_fiber_bundle.comp_homeomorph

modified def is_topological_fiber_bundle

added theorem is_trivial_topological_fiber_bundle.is_topological_fiber_bundle

added def is_trivial_topological_fiber_bundle

added theorem is_trivial_topological_fiber_bundle_fst

added theorem is_trivial_topological_fiber_bundle_snd

deleted theorem topological_fiber_bundle_core.is_topological_fiber_bundle