Add monotone-of-tendsto lemmas and OrderDual SupConvergenceClass instance

[CoolRmal]

Motivation

• Provide lemmas to deduce monotonicity of a pointwise limit from eventual or uniform monotonicity of a family of functions, to avoid duplicating such arguments elsewhere.
• Expose the duality between SupConvergenceClass and InfConvergenceClass by supplying a SupConvergenceClass instance for the order dual when the original type is an InfConvergenceClass.

Description

• Added a section with assumptions Preorder α, TopologicalSpace β, and OrderClosedTopology β and variables for a filter l and family f : ι → α → β and g : α → β.
• Implemented monotone_of_eventually_monotone_of_tendsto, which shows that if ∀ᶠ n in l, Monotone (f n) and f n x tends to g x pointwise then g is Monotone by applying le_of_tendsto to the pointwise limits.
• Implemented monotone_of_tendsto as a convenience wrapper that uses monotone_of_eventually_monotone_of_tendsto with Filter.Eventually.of_forall when every f n is monotone.
• Added an instance OrderDual.supConvergenceClass which constructs a SupConvergenceClass for αᵒᵈ from an InfConvergenceClass on α.

Testing

• Type-checked the changes by building the project (lake build / Lean compilation); the modified files compile successfully.

---

Codex Task

[chatgpt-codex-connector]

💡 Codex Review

Here are some automated review suggestions for this pull request.

Reviewed commit: 33f0b1fc77

ℹ️ About Codex in GitHub

Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you

• Open a pull request for review
• Mark a draft as ready
• Comment "@codex review".

If Codex has suggestions, it will comment; otherwise it will react with 👍.

Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".

[chatgpt-codex-connector]

Add NeBot assumption to monotone limit theorem

This theorem is currently stated for an arbitrary filter l, but it is false when l = ⊥: both hmono and each pointwise Tendsto hypothesis become vacuously true, so the lemma would force any g to be monotone. The result should require [NeBot l] (and the wrapper theorem should inherit it) so the assumptions are non-vacuous and match the intended use of le_of_tendsto-style order-closed arguments.

Useful? React with 👍 / 👎.