Theorem PartialEquiv.injective_of_source_eq_univ

Modification history

2025-11-01 19:17
Mathlib/Logic/Equiv/PartialEquiv.lean
refactor: simplify `InjOn univ f` to `Injective f` (#31024) …
Modified PartialEquiv.injective_of_source_eq_univView on Github →
2025-06-05 15:01
Mathlib/Logic/Equiv/PartialEquiv.lean
feat: One-point compactification of Euclidean space homeomorphic to sphere (#18711) …
Added PartialEquiv.injective_of_source_eq_univView on Github →