mathlib

29e7a8d5 - feat(topology/algebra/ordered, topology/algebra/infinite_sum): bounded monotone sequences converge (variant versions) (#7983)

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.