Commit 2023-07-24 16:15 5d6a12dd

View on Github →

feat: lemmas about writtenInExtChartAt (#5495)

Estimated changes

Modified Mathlib/Geometry/Manifold/SmoothManifoldWithCorners.lean

added theorem extChartAt_comp

added theorem writtenInExtChartAt_chartAt

added theorem writtenInExtChartAt_chartAt_comp

added theorem writtenInExtChartAt_chartAt_symm

added theorem writtenInExtChartAt_chartAt_symm_comp

added theorem writtenInExtChartAt_extChartAt

added theorem writtenInExtChartAt_extChartAt_symm

Modified Mathlib/Geometry/Manifold/VectorBundle/Basic.lean

added theorem FiberBundle.writtenInExtChartAt_trivializationAt

added theorem FiberBundle.writtenInExtChartAt_trivializationAt_symm