Commit 2021-11-02 10:26 541df8a0
View on Github →feat(topology/algebra/ordered/liminf_limsup): convergence of a sequence which does not oscillate infinitely (#10073)
If, for all a < b, a sequence is not frequently below a and frequently above b, then it has to converge. This is a useful convergence criterion (called no upcrossings), used for instance in martingales.
Also generalize several statements on liminfs and limsups from complete linear orders to conditionally complete linear orders.