Theorem OpenPartialHomeomorph.coe_ofContinuousOpenRestrict

Modification history

2025-12-09 05:22
Mathlib/Topology/OpenPartialHomeomorph.lean
refactor(Topology/OpenPartialHomeomorph): split long file (#32601)
Modified OpenPartialHomeomorph.coe_ofContinuousOpenRestrictView on Github →
2025-12-01 22:59
Mathlib/Topology/OpenPartialHomeomorph.lean
feat(OpenPartialHomeomorph): add missing `simp` lemmas (#32310) …
Added OpenPartialHomeomorph.coe_ofContinuousOpenRestrictView on Github →