Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-10-21 10:18 a4bbbdea

View on Github →

feat(topology/topological_fiber_bundle): topological fiber bundles (#1421)

feat(topology/topological_fiber_bundle): topological fiber bundles
better definition of fiber bundles

Estimated changes

Created src/topology/topological_fiber_bundle.lean

added theorem bundle_trivialization.continuous_at_proj

added structure bundle_trivialization

added theorem is_topological_fiber_bundle.continuous_proj

added theorem is_topological_fiber_bundle.is_open_map_proj

added def is_topological_fiber_bundle

added theorem is_topological_fiber_bundle_fst

added theorem is_topological_fiber_bundle_snd

added def topological_fiber_bundle_core.base

added theorem topological_fiber_bundle_core.continuous_proj

added def topological_fiber_bundle_core.fiber

added def topological_fiber_bundle_core.index

added theorem topological_fiber_bundle_core.is_open_map_proj

added theorem topological_fiber_bundle_core.is_topological_fiber_bundle

added def topological_fiber_bundle_core.local_triv'

added theorem topological_fiber_bundle_core.local_triv'_fst

added theorem topological_fiber_bundle_core.local_triv'_inv_fst

added theorem topological_fiber_bundle_core.local_triv'_trans

added def topological_fiber_bundle_core.local_triv

added def topological_fiber_bundle_core.local_triv_at

added def topological_fiber_bundle_core.local_triv_at_ext

added theorem topological_fiber_bundle_core.local_triv_at_ext_to_local_homeomorph

added theorem topological_fiber_bundle_core.local_triv_at_fst

added theorem topological_fiber_bundle_core.local_triv_at_symm_fst

added def topological_fiber_bundle_core.local_triv_ext

added theorem topological_fiber_bundle_core.local_triv_fst

added theorem topological_fiber_bundle_core.local_triv_symm_fst

added theorem topological_fiber_bundle_core.local_triv_trans

added theorem topological_fiber_bundle_core.mem_local_triv'_source

added theorem topological_fiber_bundle_core.mem_local_triv'_target

added theorem topological_fiber_bundle_core.mem_local_triv_at_source

added theorem topological_fiber_bundle_core.mem_local_triv_source

added theorem topological_fiber_bundle_core.mem_local_triv_target

added theorem topological_fiber_bundle_core.mem_triv_change_source

added theorem topological_fiber_bundle_core.open_source'

added theorem topological_fiber_bundle_core.open_target'

added def topological_fiber_bundle_core.proj

added def topological_fiber_bundle_core.total_space

added def topological_fiber_bundle_core.triv_change

added structure topological_fiber_bundle_core