Commit 2026-07-17 10:50 e86c4a1a

View on Github →

chore: rename OpenPartialHomeomorph.to_isOpenEmbedding (#41854) As requested in a PR review here. I also included a correction of a different docstring.

Estimated changes

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

Modified Mathlib/Topology/OpenPartialHomeomorph/Basic.lean

added theorem OpenPartialHomeomorph.isOpenEmbedding

deleted theorem OpenPartialHomeomorph.to_isOpenEmbedding