Theorem nhdsSet_singleton

Modification history

2023-08-15 15:52

Mathlib/Topology/NhdsSet.lean

feat: add `Filter.Eventually.self_of_nhdsSet` (#6497) …

Modified nhdsSet_singleton View on Github →

2023-01-27 10:13

Mathlib/Topology/NhdsSet.lean

feat: port Topology.NhdsSet (#1875)

Added nhdsSet_singleton View on Github →