Commit 2021-03-14 00:42 0c26cea2
View on Github →feat(order/filter/cofinite): a growing function has a minimum (#6556)
If tendsto f cofinite at_top, then f has a minimal element.
feat(order/filter/cofinite): a growing function has a minimum (#6556)
If tendsto f cofinite at_top, then f has a minimal element.