feat: pointwise limit of a sequence of monotone functions is monotone (#40526)

Adds lemmas showing that the pointwise limit of a sequence of frequently monotone functions is monotone in an order-closed topology. It also adds the corresponding antitone variants via the order dual.

Created with a little bit help from codex :)

Co-authored-by: Yongxi Lin <aaronlin@andrew.cmu.edu>

Author: CoolRmal

Mathlib/Topology/Order/OrderClosed.lean

@@ -48,6 +48,8 @@ see their statements.
 * `le_of_tendsto`, `ge_of_tendsto` : if `f` converges to `a` and eventually `f x ≤ b`
   (resp., `b ≤ f x`), then `a ≤ b` (resp., `b ≤ a`); we also provide primed versions
   that assume the inequalities to hold for all `x`.
+* `monotone_of_frequently_monotone_of_tendsto`, `antitone_of_frequently_antitone_of_tendsto` : the
+  pointwise limit of frequently monotone or antitone functions is monotone or antitone.
 
 ### Min, max, `sSup` and `sInf`
 
@@ -514,25 +516,54 @@ theorem IsClosed.epigraph [TopologicalSpace β] {f : β → α} {s : Set β} (hs
     (hf : ContinuousOn f s) : IsClosed { p : β × α | p.1 ∈ s ∧ f p.1 ≤ p.2 } :=
   (hs.preimage continuous_fst).isClosed_le (hf.comp continuousOn_fst Subset.rfl) continuousOn_snd
 
+section Tendsto
+
+variable {ι : Type*} {l : Filter ι} [Preorder β] {F : ι → β → α} {f : β → α} {s : Set β}
+
+/-- The limit of a collection of functions that is frequently monotone on a set is monotone on
+that set. -/
+lemma monotoneOn_of_frequently_monotoneOn_of_tendsto (hF : ∃ᶠ i in l, MonotoneOn (F i) s)
+    (hlim : ∀ x ∈ s, Tendsto (fun i ↦ F i x) l (𝓝 (f x))) : MonotoneOn f s :=
+  fun a ha b hb hab ↦ le_of_tendsto_of_tendsto_of_frequently (hlim a ha) (hlim b hb) <|
+    hF.mono fun _ hi ↦ hi ha hb hab
+
+/-- The limit of a collection of functions that is frequently monotone is monotone. -/
+lemma monotone_of_frequently_monotone_of_tendsto (hF : ∃ᶠ i in l, Monotone (F i))
+    (hlim : ∀ x, Tendsto (fun i ↦ F i x) l (𝓝 (f x))) : Monotone f :=
+  monotoneOn_univ.1 <| monotoneOn_of_frequently_monotoneOn_of_tendsto
+    (hF.mono fun _ hi ↦ hi.monotoneOn _) fun x _ ↦ hlim x
+
+/-- The limit of a collection of functions that is frequently antitone on a set is antitone on
+that set. -/
+lemma antitoneOn_of_frequently_antitoneOn_of_tendsto (hF : ∃ᶠ i in l, AntitoneOn (F i) s)
+    (hlim : ∀ x ∈ s, Tendsto (fun i ↦ F i x) l (𝓝 (f x))) : AntitoneOn f s :=
+  monotoneOn_of_frequently_monotoneOn_of_tendsto (α := αᵒᵈ) hF hlim
+
+/-- The limit of a collection of functions that is frequently antitone is antitone. -/
+lemma antitone_of_frequently_antitone_of_tendsto (hF : ∃ᶠ i in l, Antitone (F i))
+    (hlim : ∀ x, Tendsto (fun i ↦ F i x) l (𝓝 (f x))) : Antitone f :=
+  monotone_of_frequently_monotone_of_tendsto (α := αᵒᵈ) hF hlim
+
 /-- The set of monotone functions on a set is closed. -/
-theorem isClosed_monotoneOn [Preorder β] {s : Set β} : IsClosed {f : β → α | MonotoneOn f s} := by
+theorem isClosed_monotoneOn : IsClosed {f : β → α | MonotoneOn f s} := by
   simp only [isClosed_iff_clusterPt, clusterPt_principal_iff_frequently]
-  intro g hg a ha b hb hab
-  have hmain (x) : Tendsto (fun f' ↦ f' x) (𝓝 g) (𝓝 (g x)) := continuousAt_apply x _
-  exact le_of_tendsto_of_tendsto_of_frequently (hmain a) (hmain b) (hg.mono fun g h ↦ h ha hb hab)
+  exact fun g hg => monotoneOn_of_frequently_monotoneOn_of_tendsto hg
+    fun x _ ↦ continuousAt_apply x g
 
 /-- The set of monotone functions is closed. -/
-theorem isClosed_monotone [Preorder β] : IsClosed {f : β → α | Monotone f} := by
+theorem isClosed_monotone : IsClosed {f : β → α | Monotone f} := by
   simp_rw [← monotoneOn_univ]
   exact isClosed_monotoneOn
 
 /-- The set of antitone functions on a set is closed. -/
-theorem isClosed_antitoneOn [Preorder β] {s : Set β} : IsClosed {f : β → α | AntitoneOn f s} :=
-  isClosed_monotoneOn (α := αᵒᵈ) (β := β)
+theorem isClosed_antitoneOn : IsClosed {f : β → α | AntitoneOn f s} :=
+  isClosed_monotoneOn (α := αᵒᵈ)
 
 /-- The set of antitone functions is closed. -/
-theorem isClosed_antitone [Preorder β] : IsClosed {f : β → α | Antitone f} :=
-  isClosed_monotone (α := αᵒᵈ) (β := β)
+theorem isClosed_antitone : IsClosed {f : β → α | Antitone f} :=
+  isClosed_monotone (α := αᵒᵈ)
+
+end Tendsto
 
 end Preorder