Theorem Set.InjOn.exists_mem_nhdsSet

Modification history

2024-12-18 10:57
Mathlib/Topology/Separation/Basic.lean
chore(Topology/Separation): split large file (#20031) …
Modified Set.InjOn.exists_mem_nhdsSetView on Github →
2023-10-30 11:10
Mathlib/Topology/Separation.lean
feat: add `Set.InjOn.exists_mem_nhdsSet` (#7947) …
Added Set.InjOn.exists_mem_nhdsSetView on Github →