Theorem Set.Ici_eq_singleton_iff_isTop

Modification history

2023-08-31 13:03
Mathlib/Data/Set/Intervals/Basic.lean
feat: the atTop filter is countably generated in a second-countable topology (#6864)
Added Set.Ici_eq_singleton_iff_isTopView on Github →