refactor(Probability/Kernel/CondCdf): mv tendsto_of_antitone (#10046)

Co-authored-by: Moritz Firsching <[email protected]>
leanprover-community · Jan 29, 2024 · 00b71ef · 00b71ef
1 parent 68c771a
commit 00b71ef
Show file tree

Hide file tree

Showing 2 changed files with 6 additions and 7 deletions.
diff --git a/Mathlib/Probability/Kernel/CondCdf.lean b/Mathlib/Probability/Kernel/CondCdf.lean
@@ -87,13 +87,6 @@ theorem atTop_le_nhds_top {α : Type*} [TopologicalSpace α] [LinearOrder α] [O
   @atBot_le_nhds_bot αᵒᵈ _ _ _ _
 #align at_top_le_nhds_top atTop_le_nhds_top
 
--- todo: move to topology/algebra/order/monotone_convergence
-theorem tendsto_of_antitone {ι α : Type*} [Preorder ι] [TopologicalSpace α]
-    [ConditionallyCompleteLinearOrder α] [OrderTopology α] {f : ι → α} (h_mono : Antitone f) :
-    Tendsto f atTop atBot ∨ ∃ l, Tendsto f atTop (𝓝 l) :=
-  @tendsto_of_monotone ι αᵒᵈ _ _ _ _ _ h_mono
-#align tendsto_of_antitone tendsto_of_antitone
-
 -- todo: move to measure_theory/measurable_space
 /-- Monotone convergence for an infimum over a directed family and indexed by a countable type -/
 theorem lintegral_iInf_directed_of_measurable {mα : MeasurableSpace α} [Countable β]

diff --git a/Mathlib/Topology/Algebra/Order/MonotoneConvergence.lean b/Mathlib/Topology/Algebra/Order/MonotoneConvergence.lean
@@ -227,6 +227,12 @@ theorem tendsto_of_monotone {ι α : Type*} [Preorder ι] [TopologicalSpace α]
   else Or.inl <| tendsto_atTop_atTop_of_monotone' h_mono H
 #align tendsto_of_monotone tendsto_of_monotone
 
+theorem tendsto_of_antitone {ι α : Type*} [Preorder ι] [TopologicalSpace α]
+    [ConditionallyCompleteLinearOrder α] [OrderTopology α] {f : ι → α} (h_mono : Antitone f) :
+    Tendsto f atTop atBot ∨ ∃ l, Tendsto f atTop (𝓝 l) :=
+  @tendsto_of_monotone ι αᵒᵈ _ _ _ _ _ h_mono
+#align tendsto_of_antitone tendsto_of_antitone
+
 theorem tendsto_iff_tendsto_subseq_of_monotone {ι₁ ι₂ α : Type*} [SemilatticeSup ι₁] [Preorder ι₂]
     [Nonempty ι₁] [TopologicalSpace α] [ConditionallyCompleteLinearOrder α] [OrderTopology α]
     [NoMaxOrder α] {f : ι₂ → α} {φ : ι₁ → ι₂} {l : α} (hf : Monotone f)