Theorem Set.Ici_eq_singleton_iff_isTop

Modification history

2025-04-02 09:50
Mathlib/Order/Interval/Set/Basic.lean
chore: split `Order.Interval.Set.Basic` (#23556) …
Modified Set.Ici_eq_singleton_iff_isTopView on Github →
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 →