Commit 2026-02-27 22:05 861e4dad

View on Github →

feat(Geometry/Manifold): API for extended coordinate changes (#35391) Introduce a definition I.extendCoordChange e e' for what previously appeared in lemmas as (e.extend I).symm ≫ e'.extend I, and provide some more API lemmas. Split out from #33189.

Estimated changes

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

added theorem ModelWithCorners.contDiffOn_extendCoordChange

added theorem ModelWithCorners.contDiffOn_extendCoordChange_symm

added theorem ModelWithCorners.contDiffWithinAt_extendCoordChange'

added theorem ModelWithCorners.contDiffWithinAt_extendCoordChange

added theorem ModelWithCorners.extendCoordChange_source

added theorem ModelWithCorners.extendCoordChange_source_mem_nhdsWithin'

added theorem ModelWithCorners.extendCoordChange_source_mem_nhdsWithin

added theorem ModelWithCorners.extendCoordChange_symm

added theorem ModelWithCorners.extendCoordChange_target

added theorem ModelWithCorners.isInvertible_fderivWithin_extendCoordChange

added theorem ModelWithCorners.uniqueDiffOn_extendCoordChange_source

added theorem ModelWithCorners.uniqueDiffOn_extendCoordChange_target

deleted theorem OpenPartialHomeomorph.contDiffOn_extend_coord_change

deleted theorem OpenPartialHomeomorph.contDiffWithinAt_extend_coord_change'

deleted theorem OpenPartialHomeomorph.contDiffWithinAt_extend_coord_change

deleted theorem OpenPartialHomeomorph.extend_coord_change_source

deleted theorem OpenPartialHomeomorph.extend_coord_change_source_mem_nhdsWithin'

deleted theorem OpenPartialHomeomorph.extend_coord_change_source_mem_nhdsWithin

modified theorem OpenPartialHomeomorph.extend_image_source_inter

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

Modified scripts/nolints_prime_decls.txt