Theorem nhds_is_closed
Modification history
2022-09-20 05:26
src/topology/separation.lean
feat(topology/separation): define `regular_space` (#16360)
Deleted nhds_is_closedView on Github →2022-07-13 00:00
src/topology/separation.lean
refactor(topology/separation): rename `regular_space` to `t3_space` (#15169) …
Modified nhds_is_closedView on Github →2019-11-12 11:23
src/topology/separation.lean
style(*): use notation `𝓝` for `nhds` (#1582) …
Modified nhds_is_closedView on Github →2019-03-08 08:46
src/topology/separation.lean
feat(*): has_mem (set α) (filter α) (#799)
Modified nhds_is_closedView on Github →