Commit 2025-07-04 16:21 2cea46de

View on Github →

feat: more API on manifolds (#26501)

Estimated changes

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

Modified Mathlib/Geometry/Manifold/IsManifold/ExtChartAt.lean

added theorem PartialHomeomorph.extend_preimage_mem_nhds_of_mem_nhdsWithin

added theorem extChartAt_preimage_mem_nhds_of_mem_nhdsWithin

Modified Mathlib/Geometry/Manifold/MFDeriv/Atlas.lean

added theorem TangentBundle.continuousLinearMapAt_trivializationAt

added theorem TangentBundle.symmL_trivializationAt

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

added theorem TangentBundle.continuousLinearMapAt_trivializationAt_eq_core

added theorem TangentBundle.symmL_trivializationAt_eq_core

deleted theorem TangentBundle.trivializationAt_continuousLinearMapAt

deleted theorem TangentBundle.trivializationAt_symmL