Commit 2025-12-01 22:59 91b78e4d

View on Github →

feat(OpenPartialHomeomorph): add missing simp lemmas (#32310) I found missing lemmas about restrOpen while working on https://github.com/urkud/SardMoreira.

Estimated changes

Modified Mathlib/Topology/OpenPartialHomeomorph.lean

added theorem OpenPartialHomeomorph.coe_ofContinuousOpen

added theorem OpenPartialHomeomorph.coe_ofContinuousOpenRestrict

added theorem OpenPartialHomeomorph.coe_ofContinuousOpenRestrict_symm

added theorem OpenPartialHomeomorph.coe_ofContinuousOpen_symm

added theorem OpenPartialHomeomorph.coe_restrOpen

added theorem OpenPartialHomeomorph.coe_restrOpen_symm