Theorem OpenPartialHomeomorph.isOpenEmbedding_restrict

Modification history

2026-07-20 20:28
Mathlib/Topology/OpenPartialHomeomorph/Basic.lean
feat: generalize `Topology/OpenPartialHomeomorph/Basic` to `PartialHomeomorph` (#41045) …
Modified OpenPartialHomeomorph.isOpenEmbedding_restrictView on Github →
2026-07-20 01:34
Mathlib/Topology/OpenPartialHomeomorph/Basic.lean
refactor: rename restrict to domRestrict (#25980) …
Modified OpenPartialHomeomorph.isOpenEmbedding_restrictView on Github →
2025-12-09 05:22
Mathlib/Topology/OpenPartialHomeomorph.lean
refactor(Topology/OpenPartialHomeomorph): split long file (#32601)
Modified OpenPartialHomeomorph.isOpenEmbedding_restrictView on Github →
2025-10-02 09:10
Mathlib/Topology/OpenPartialHomeomorph.lean
chore: rename PartialHomeomorph to OpenPartialHomeomorph (#29113) …
Added OpenPartialHomeomorph.isOpenEmbedding_restrictView on Github →