Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-07-09 21:17 d6e9f97b

View on Github →

feat(topology/basic): yet another mem_closure (#3348)

Estimated changes

Modified src/order/filter/basic.lean

modified theorem filter.comap_ne_bot

added theorem filter.comap_ne_bot_iff

Modified src/topology/basic.lean

added theorem mem_closure_iff_comap_ne_bot