Commit 2026-04-03 17:21 8f1377de

feat(Topology/Order): existence of a sequence that converges to limsup (#37296) The PR establishes the following results:

1. The limsSup of a filter f is a cluster point of f, and in fact it is the greatest cluster point of f.
2. If f is a countably generated filter in a first countable space, then there exists a sequence converging to limsSup f.
3. Analogous statements for limsup are also proved.
4. Analogous statements for limsInf and liminf are also proved. Zulip discussion: #Is there code for X? > Existence of a subsequence that tendsto liminf