From 00b71ef0d839c33562fac640420086f01a428b29 Mon Sep 17 00:00:00 2001 From: Moritz Firsching Date: Mon, 29 Jan 2024 14:47:04 +0000 Subject: [PATCH] refactor(Probability/Kernel/CondCdf): mv tendsto_of_antitone (#10046) Co-authored-by: Moritz Firsching --- Mathlib/Probability/Kernel/CondCdf.lean | 7 ------- Mathlib/Topology/Algebra/Order/MonotoneConvergence.lean | 6 ++++++ 2 files changed, 6 insertions(+), 7 deletions(-) diff --git a/Mathlib/Probability/Kernel/CondCdf.lean b/Mathlib/Probability/Kernel/CondCdf.lean index 6761907573254..eab928e31c06b 100644 --- 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 index 6c16cd2a12183..6ba1a6eee4ada 100644 --- 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)