Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2023-03-28 23:45 01876449

View on Github →

feat(geometry/manifold/vector_bundle/tangent): use the new tangent bundle definition in the library (#18601)

  • Stop using the old tangent bundle definition, and use the new one instead
  • This affects geometry.manifold.mfderiv and later files.
  • We remove cont_mdiff_at_iff_target, which doesn't hold anymore in the new setting.
  • We prove cont_mdiff_at_total_space, which characterizes C^n maps into a vector bundle. We need a bunch of basic lemmas to prove this. This makes it easy to prove smooth_zero_section.
  • We move some results from cont_mdiff_mfderiv to manifold/vector_bundle/basic

Estimated changes

deleted def tangent_bundle.proj
deleted theorem tangent_bundle.proj_apply
deleted def tangent_bundle
deleted def tangent_bundle_core
deleted theorem tangent_bundle_proj_open
deleted def tangent_space
added def tangent_bundle
added def tangent_space