mathlib3

5008de8b - feat(order): some properties about monotone predicates (#11904)

feat(order): some properties about monotone predicates (#11904) * We prove that some predicates are monotone/antitone w.r.t. some order. The proofs are all trivial. * We prove 2 `iff` statements depending on the hypothesis that a certain predicate is (anti)mono: `exists_ge_and_iff_exists` and `filter.exists_mem_and_iff`) * The former is used to prove `bdd_above_iff_exists_ge`, the latter will be used in a later PR.