Mathlib v3 is deprecated. Go to Mathlib v4

Theorem mem_nhds_discrete

Modification history

2022-03-18 21:54
src/topology/order.lean
feat(topology/{order,separation}): several lemmas from an old branch (#12794) …
Added mem_nhds_discreteView on Github →