Commit 2021-06-18 15:33 29e7a8d5

feat(topology/algebra/ordered, topology/algebra/infinite_sum): bounded monotone sequences converge (variant versions) (#7983) A bounded monotone sequence converges to a value a, if and only if a is a least upper bound for its range. Mathlib had several variants of this fact previously (phrased in terms of, eg, csupr), but not quite this version (phrased in terms of has_lub). This version has a couple of advantages:

• it applies to more general typeclasses (eg, linear_order) where the existence of suprema is not in general known
• it applies to algebraic typeclasses (linear_ordered_add_comm_monoid, etc) where, since completeness of orders is not a mix-in, it is not possible to simultaneously assume (conditionally_)complete_linear_order The latter point makes these lemmas useful when dealing with tsum. We get: a nonnegative function f satisfies has_sum f a, if and only if a is a least upper bound for its partial sums.