mathlib3

0c26cea2 - feat(order/filter/cofinite): a growing function has a minimum (#6556)

feat(order/filter/cofinite): a growing function has a minimum (#6556) If `tendsto f cofinite at_top`, then `f` has a minimal element. Co-authored-by: Heather Macbeth <25316162+hrmacbeth@users.noreply.github.com> Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr>