feat: add tendsto_iff_tendsto_subseq_of_antitone (#11200)

Add `tendsto_iff_tendsto_subseq_of_antitone`, next to `tendsto_iff_tendsto_subseq_of_monotone`.



Co-authored-by: Rémy Degenne <remydegenne@gmail.com>

Mathlib/Topology/Algebra/Order/MonotoneConvergence.lean

@@ -244,6 +244,12 @@ theorem tendsto_iff_tendsto_subseq_of_monotone {ι₁ ι₂ α : Type*} [Semilat
     · rwa [tendsto_nhds_unique h (hl'.comp hg)]
 #align tendsto_iff_tendsto_subseq_of_monotone tendsto_iff_tendsto_subseq_of_monotone
 
+theorem tendsto_iff_tendsto_subseq_of_antitone {ι₁ ι₂ α : Type*} [SemilatticeSup ι₁] [Preorder ι₂]
+    [Nonempty ι₁] [TopologicalSpace α] [ConditionallyCompleteLinearOrder α] [OrderTopology α]
+    [NoMinOrder α] {f : ι₂ → α} {φ : ι₁ → ι₂} {l : α} (hf : Antitone f)
+    (hg : Tendsto φ atTop atTop) : Tendsto f atTop (𝓝 l) ↔ Tendsto (f ∘ φ) atTop (𝓝 l) :=
+  tendsto_iff_tendsto_subseq_of_monotone (α := αᵒᵈ) hf hg
+
 /-! The next family of results, such as `isLUB_of_tendsto_atTop` and `iSup_eq_of_tendsto`, are
 converses to the standard fact that bounded monotone functions converge. They state, that if a
 monotone function `f` tends to `a` along `Filter.atTop`, then that value `a` is a least upper bound