Commit 2022-09-02 04:12 525c5a81

View on Github →

feat(topology/fiber_bundle): Each fiber of a trivialization is homeomorphic to the specified fiber (#16079) This PR adds topological_fiber_bundle.trivialization.preimage_singleton_homeomorph, which states that each fiber of a trivialization is homeomorphic to the specified fiber.

Estimated changes

Modified src/topology/fiber_bundle.lean

added theorem topological_fiber_bundle.trivialization.image_preimage_eq_prod_univ

added def topological_fiber_bundle.trivialization.preimage_homeomorph

added theorem topological_fiber_bundle.trivialization.preimage_homeomorph_apply

added theorem topological_fiber_bundle.trivialization.preimage_homeomorph_symm_apply

added def topological_fiber_bundle.trivialization.preimage_singleton_homeomorph

added theorem topological_fiber_bundle.trivialization.preimage_singleton_homeomorph_apply

added theorem topological_fiber_bundle.trivialization.preimage_singleton_homeomorph_symm_apply

added theorem topological_fiber_bundle.trivialization.preimage_subset_source

added def topological_fiber_bundle.trivialization.source_homeomorph_base_set_prod

added theorem topological_fiber_bundle.trivialization.source_homeomorph_base_set_prod_apply

added theorem topological_fiber_bundle.trivialization.source_homeomorph_base_set_prod_symm_apply

Modified src/topology/homeomorph.lean

added def homeomorph.homeomorph_of_unique

Modified src/topology/local_homeomorph.lean

added def local_homeomorph.homeomorph_of_image_subset_source