Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2023-04-25 17:43 d2d964c6

View on Github →

feat(topology/vector_bundle/basic): define in_coordinates (#18826)

From the sphere eversion project

Estimated changes

Modified src/topology/vector_bundle/basic.lean

added def continuous_linear_map.in_coordinates

added theorem continuous_linear_map.in_coordinates_eq

Modified src/topology/vector_bundle/hom.lean

deleted def bundle.continuous_linear_map

added theorem hom_trivialization_at_apply

added theorem hom_trivialization_at_source

added theorem hom_trivialization_at_target