mathlib

c543ec9a - feat(topology/algebra/ordered/basic): sequences tending to Inf/Sup (#8524)

feat(topology/algebra/ordered/basic): sequences tending to Inf/Sup (#8524) We show that there exist monotone sequences tending to the Inf/Sup of a set in a conditionally complete linear order, as well as several related lemmas expressed in terms of `is_lub` and `is_glb`.