Theorem PartialEquiv.toEquiv_eq_codRestrict_restrict

Modification history

2026-07-20 20:28
Mathlib/Logic/Equiv/PartialEquiv.lean
feat: generalize `Topology/OpenPartialHomeomorph/Basic` to `PartialHomeomorph` (#41045) …
Added PartialEquiv.toEquiv_eq_codRestrict_restrictView on Github →