feat(*): add various order-related lemmas

[ocfnash]

These all came up while preparing to introduce the definition of ergodic maps but it seems better to PR them separately.

---

[ocfnash]

Note that in the review #16819 discussed on Zulip I agreed to reduce use of dot notation and to reorder the arguments in filter.limsup and filter.liminf. I'll apply these changes here if necessary, depending on which PR lands first.

[bors[bot]]

:v: ocfnash can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

[ocfnash]

At it happens #16819 is now on its way to bors so this PR will have to wait and merge master once #16819 has landed.

[YaelDillies]

Thank you very much for bearing with this lengthy review!

maintainer merge

[github-actions[bot]]

🚀 Pull request has been placed on the maintainer queue by YaelDillies.

[dupuisf]

bors r+

[bors[bot]]

Build failed (retrying...):

• Lint mathlib

[bors[bot]]

Pull request successfully merged into master.

Build succeeded:

• Build mathlib
• Lint mathlib
• Lint style
• Run tests