Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-02-24 12:56 8429ec96

View on Github →

feat(topology/vector_bundle): topological_vector_prebundle (#8154) In this PR we implement a new standard construction for topological vector bundles: namely a structure that permits to define a vector 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 vector bundle structure for which the local equivalences are also local homeomorphism and hence local trivializations.

Estimated changes

Modified src/data/bundle.lean

modified def bundle.proj

Modified src/data/set/function.lean

added theorem set.restrict_comp_cod_restrict

Modified src/topology/constructions.lean

added theorem continuous.cod_restrict

added theorem inducing.of_cod_restrict

added theorem inducing_coe

Modified src/topology/fiber_bundle.lean

Modified src/topology/local_homeomorph.lean

added theorem local_homeomorph.continuous_iff_continuous_comp_left

Modified src/topology/vector_bundle.lean

added structure topological_vector_bundle.pretrivialization

added def topological_vector_bundle.trivialization.to_pretrivialization

added theorem topological_vector_prebundle.continuous_total_space_mk

added theorem topological_vector_prebundle.inducing_total_space_mk_of_inducing_comp

added theorem topological_vector_prebundle.mem_trivialization_at_source

added def topological_vector_prebundle.to_topological_fiber_prebundle

added theorem topological_vector_prebundle.to_topological_vector_bundle

added theorem topological_vector_prebundle.total_space_mk_preimage_source

added def topological_vector_prebundle.total_space_topology

added def topological_vector_prebundle.trivialization_at

added structure topological_vector_prebundle