Theorem OpenPartialHomeomorph.coe_restrOpen

Modification history

2025-12-09 05:22

Mathlib/Topology/OpenPartialHomeomorph.lean

refactor(Topology/OpenPartialHomeomorph): split long file (#32601)

Modified OpenPartialHomeomorph.coe_restrOpen View on Github →

2025-12-01 22:59

Mathlib/Topology/OpenPartialHomeomorph.lean

feat(OpenPartialHomeomorph): add missing `simp` lemmas (#32310) …

Added OpenPartialHomeomorph.coe_restrOpen View on Github →