Commit 2026-05-28 11:18 106cea40

View on Github →

chore: rename some OpenPartialHomeomorph declarations (#39565) In the review of #39084, a few suggested renames relating to OpenPartialHomeomorph came up which I am doing in this PR.

Estimated changes

Modified Mathlib/Analysis/InnerProductSpace/Calculus.lean

Modified Mathlib/Geometry/Manifold/ContMDiff/Defs.lean

Modified Mathlib/Geometry/Manifold/ContMDiffMFDeriv.lean

Modified Mathlib/Geometry/Manifold/Instances/Icc.lean

Modified Mathlib/Geometry/Manifold/Instances/Sphere.lean

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

Modified Mathlib/Geometry/Manifold/LocalDiffeomorph.lean

Modified Mathlib/Geometry/Manifold/LocalInvariantProperties.lean

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

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

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

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

Modified Mathlib/Logic/Equiv/PartialEquiv.lean

added theorem PartialEquiv.mapsTo_symm

deleted theorem PartialEquiv.symm_mapsTo

Modified Mathlib/Topology/OpenPartialHomeomorph/Composition.lean

Modified Mathlib/Topology/OpenPartialHomeomorph/Constructions.lean

Modified Mathlib/Topology/OpenPartialHomeomorph/Defs.lean

deleted theorem OpenPartialHomeomorph.coe_coe

deleted theorem OpenPartialHomeomorph.coe_coe_symm

added theorem OpenPartialHomeomorph.coe_mk

added theorem OpenPartialHomeomorph.coe_mk_symm

added theorem OpenPartialHomeomorph.coe_toPartialEquiv

added theorem OpenPartialHomeomorph.coe_toPartialEquiv_symm

deleted theorem OpenPartialHomeomorph.mk_coe

deleted theorem OpenPartialHomeomorph.mk_coe_symm

deleted def OpenPartialHomeomorph.replaceEquiv

deleted theorem OpenPartialHomeomorph.replaceEquiv_eq_self

added def OpenPartialHomeomorph.replacePartialEquiv

added theorem OpenPartialHomeomorph.replacePartialEquiv_eq_self