Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2023-05-17 16:46 c89fe2d5

View on Github →

feat(geometry/manifold/vector_bundle/hom): the hom bundle is smooth (#18828)

From the sphere eversion project

Estimated changes

Modified src/geometry/manifold/vector_bundle/basic.lean

added theorem vector_prebundle.mk_smooth_coord_change

added theorem vector_prebundle.smooth_coord_change_apply

added theorem vector_prebundle.smooth_on_smooth_coord_change

added theorem vector_prebundle.smooth_vector_bundle

Created src/geometry/manifold/vector_bundle/hom.lean

added theorem cont_mdiff_at_hom_bundle

added theorem hom_chart

added theorem smooth_at_hom_bundle

added theorem smooth_on_continuous_linear_map_coord_change

added def smooth_vector_bundle.continuous_linear_map.aux