Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2023-04-22 07:09 7dfe8583

View on Github →

feat(geometry/manifold/vector_bundle/tangent): some equations about trivializations (#18825)

From the sphere eversion project

Estimated changes

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

added theorem tangent_bundle.continuous_linear_map_at_model_space

added theorem tangent_bundle.coord_change_model_space

added theorem tangent_bundle.symmL_model_space

added theorem tangent_bundle.trivialization_at_continuous_linear_map_at

added theorem tangent_bundle.trivialization_at_symmL

added theorem tangent_bundle_core_coord_change_model_space

Modified src/topology/vector_bundle/basic.lean

added theorem vector_bundle_core.local_triv_continuous_linear_map_at

added theorem vector_bundle_core.local_triv_symmL

deleted def vector_bundle_core.proj

deleted def vector_bundle_core.total_space

added theorem vector_bundle_core.trivialization_at_continuous_linear_map_at

added theorem vector_bundle_core.trivialization_at_coord_change_eq

added theorem vector_bundle_core.trivialization_at_symmL