Add monotone_of_tendsto and monotone_of_tendsto_of_eventually lemmas

[CoolRmal]

Motivation

• Provide a simple criterion to deduce Monotone f from a family F i which is eventually monotone (or each F i is monotone) and converges pointwise to f, so monotonicity can be transferred from approximating nets to the limit.

Description

• Add @[to_dual] theorem monotone_of_tendsto_of_eventually and @[to_dual] theorem monotone_of_tendsto to Mathlib/Topology/Order/MonotoneConvergence.lean, which infer Monotone f from eventual order-preservation of F along a nontrivial filter l (or from each F i being Monotone) together with Tendsto (fun i => F i a) l (𝓝 (f a)) for every a, and prove the result via tendsto_le_of_eventuallyLE.

Testing

• No automated tests were run for this change.

---

Codex Task