Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-06-22 13:46 d939b0e6

View on Github →

feat(topology/vector_bundle/hom): define the vector bundle of continuous linear maps (#14541)

The changes in topology/fiber_bundle are not necessary for this PR, but perhaps nice additions
Co-authored by: Heather Macbeth 25316162+hrmacbeth@users.noreply.github.com
Co-authored by: Patrick Massot patrick.massot@u-psud.fr

Estimated changes

Modified src/topology/fiber_bundle.lean

added theorem topological_fiber_bundle.pretrivialization.symm_apply_apply

added theorem topological_fiber_bundle.pretrivialization.target_inter_preimage_symm_source_eq

added theorem topological_fiber_bundle.pretrivialization.trans_source

added theorem topological_fiber_bundle.trivialization.continuous_at_of_comp_left

added theorem topological_fiber_bundle.trivialization.continuous_at_of_comp_right

added theorem topological_fiber_prebundle.continuous_on_of_comp_right

Modified src/topology/vector_bundle/basic.lean

Created src/topology/vector_bundle/hom.lean

added def bundle.continuous_linear_map.topological_vector_prebundle

added def bundle.continuous_linear_map

added def topological_vector_bundle.pretrivialization.continuous_linear_map

added theorem topological_vector_bundle.pretrivialization.continuous_linear_map_apply

added def topological_vector_bundle.pretrivialization.continuous_linear_map_coord_change

added theorem topological_vector_bundle.pretrivialization.continuous_linear_map_coord_change_apply

added theorem topological_vector_bundle.pretrivialization.continuous_linear_map_symm_apply'

added theorem topological_vector_bundle.pretrivialization.continuous_linear_map_symm_apply

added theorem topological_vector_bundle.pretrivialization.continuous_on_continuous_linear_map_coord_change

added theorem topological_vector_bundle.trivialization.base_set_continuous_linear_map

added def topological_vector_bundle.trivialization.continuous_linear_map

added theorem topological_vector_bundle.trivialization.continuous_linear_map_apply