mathlib

b4502fd1 - feat(topology): is_open and is_closed in term of ∀ᶠ and ∃ᶠ (#16545)