Skip to content

Commit a7d30c2

Browse files
scholzhannahthemathqueen
authored andcommitted
chore(OpenPartialHomeomorph): add missing deprecation (leanprover-community#39968)
Add deprecation that I forgot in leanprover-community#39565. Co-authored-by: Monica Omar <23701951+themathqueen@users.noreply.github.com>
1 parent a6445f0 commit a7d30c2

1 file changed

Lines changed: 2 additions & 0 deletions

File tree

  • Mathlib/Topology/OpenPartialHomeomorph

Mathlib/Topology/OpenPartialHomeomorph/Defs.lean

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -167,6 +167,8 @@ protected theorem mapsTo : MapsTo e e.source e.target := fun _ => e.map_source
167167
protected theorem mapsTo_symm : MapsTo e.symm e.target e.source :=
168168
e.symm.mapsTo
169169

170+
@[deprecated (since := "2026-05-28")] alias symm_mapsTo := OpenPartialHomeomorph.mapsTo_symm
171+
170172
protected theorem leftInvOn : LeftInvOn e.symm e e.source := fun _ => e.left_inv
171173

172174
protected theorem rightInvOn : RightInvOn e.symm e e.target := fun _ => e.right_inv

0 commit comments

Comments
 (0)