Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
feat(Geometry/Manifold/VectorBundle/Tangent): tangentCoordChange (#8672)
We define `tangentCoordChange` as a convenient abbreviation for coordinate changes on the tangent bundle. We also restate the axioms of `VectorBundleCore` as lemmas involving `extChartAt`. Currently, we need to write `(tangentBundleCore I M).coordChange (achart H x) (achart H y)`, referring explicitly to the atlas of `M`. Since `tangentBundleCore` uses the same base sets as the preferred charts of the base manifold, we wish to work directly with points `x y : M` and the preferred extended charts at those points (`extChartAt`). We find this definition and related lemmas useful in #8483 in shortening proofs.
- Loading branch information