Commit 2021-06-30 21:21 ad00a021

View on Github →

feat(topology/vector_bundle): topological_vector_bundle_core (#8089) Analogous construction to topological_fiber_bundle_core. This construction gives a way to construct vector bundles from a structure registering how trivialization changes act on fibers.

Estimated changes

Modified src/topology/vector_bundle.lean

added def topological_vector_bundle_core.base

added theorem topological_vector_bundle_core.coe_cord_change

added theorem topological_vector_bundle_core.continuous_proj

added theorem topological_vector_bundle_core.coord_change_linear_comp

added def topological_vector_bundle_core.fiber

added def topological_vector_bundle_core.index

added theorem topological_vector_bundle_core.is_open_map_proj

added def topological_vector_bundle_core.local_triv

added def topological_vector_bundle_core.local_triv_at

added theorem topological_vector_bundle_core.local_triv_at_apply

added theorem topological_vector_bundle_core.mem_local_triv_source

added theorem topological_vector_bundle_core.mem_source_at

added theorem topological_vector_bundle_core.mem_triv_change_source

added def topological_vector_bundle_core.proj

added def topological_vector_bundle_core.to_topological_vector_bundle_core

added def topological_vector_bundle_core.triv_change

added structure topological_vector_bundle_core