mathlib

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