Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2023-03-09 17:31 ddec54a7

View on Github →

feat(geometry/manifold/vector_bundle/tangent): the tangent bundle is a smooth vector bundle (#17680)

This defines a tangent bundle as a smooth vector bundle
Currently we still use the old definition in the library (e.g. for mfderiv). Therefore we put the new version temporarily in the hidden namespace, to avoid a name clash (we could skip this PR and immediately merge #18068, but that will be a big PR). Co-authored by: Heather Macbeth 25316162+hrmacbeth@users.noreply.github.com

Estimated changes

Modified src/analysis/calculus/fderiv.lean

added theorem fderiv_within_fderiv_within

Modified src/geometry/manifold/smooth_manifold_with_corners.lean

added theorem local_homeomorph.cont_diff_within_at_extend_coord_change'

added theorem local_homeomorph.extend_coord_change_source_mem_nhds_within'

added theorem local_homeomorph.extend_coord_change_source_mem_nhds_within

added theorem local_homeomorph.extend_left_inv

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

added theorem fiber_bundle.charted_space_chart_at

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

added theorem hidden.cont_diff_on_fderiv_coord_change

added def hidden.tangent_bundle

added def hidden.tangent_bundle_core

added theorem hidden.tangent_bundle_core_coord_change_achart

added theorem hidden.tangent_bundle_model_space_chart_at

added theorem hidden.tangent_bundle_model_space_coe_chart_at

added theorem hidden.tangent_bundle_model_space_coe_chart_at_symm

added def hidden.tangent_bundle_model_space_homeomorph

added theorem hidden.tangent_bundle_model_space_homeomorph_coe

added theorem hidden.tangent_bundle_model_space_homeomorph_coe_symm

added def hidden.tangent_space

added theorem hidden.tangent_space_chart_at

added theorem hidden.tangent_space_chart_at_to_local_equiv