doc-next-gen

Mathlib.Topology.Order.MonotoneConvergence

Module docstring

{"# Bounded monotone sequences converge

In this file we prove a few theorems of the form “if the range of a monotone function f : ι → α admits a least upper bound a, then f x tends to a as x → ∞”, as well as version of this statement for (conditionally) complete lattices that use ⨆ x, f x instead of IsLUB.

These theorems work for linear orders with order topologies as well as their products (both in terms of Prod and in terms of function types). In order to reduce code duplication, we introduce two typeclasses (one for the property formulated above and one for the dual property), prove theorems assuming one of these typeclasses, and provide instances for linear orders and their products.

We also prove some \"inverse\" results: if f n is a monotone sequence and a is its limit, then f n ≤ a for all n.

Tags

monotone convergence ","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 for the range of f.

Related theorems above (IsLUB.isLUB_of_tendsto, IsGLB.isGLB_of_tendsto etc) cover the case when f x tends to a as x tends to some point b in the domain. "}

SupConvergenceClass structure
(α : Type*) [Preorder α] [TopologicalSpace α]
Full source 
/-- We say that `α` is a `SupConvergenceClass` if the following holds. Let `f : ι → α` be a
monotone function, let `a : α` be a least upper bound of `Set.range f`. Then `f x` tends to `𝓝 a`
 as `x → ∞` (formally, at the filter `Filter.atTop`). We require this for `ι = (s : Set α)`,
`f = (↑)` in the definition, then prove it for any `f` in `tendsto_atTop_isLUB`.

This property holds for linear orders with order topology as well as their products. -/
class SupConvergenceClass (α : Type*) [Preorder α] [TopologicalSpace α] : Prop where
  /-- proof that a monotone function tends to `𝓝 a` as `x → ∞` -/
  tendsto_coe_atTop_isLUB :
    ∀ (a : α) (s : Set α), IsLUB s a → Tendsto ((↑) : s → α) atTop (𝓝 a)
Sup-Convergence Class
Informal description
A type `α` with a preorder and a topological space structure is called a *sup-convergence class* if for any monotone function `f : ι → α` with a least upper bound `a` of its range, the function `f` tends to `a` as the input tends to infinity (i.e., along the filter `atTop`). This property is initially required for the inclusion map of a subset `s : Set α` and then generalized to any monotone function.
InfConvergenceClass structure
(α : Type*) [Preorder α] [TopologicalSpace α]
Full source 
/-- We say that `α` is an `InfConvergenceClass` if the following holds. Let `f : ι → α` be a
monotone function, let `a : α` be a greatest lower bound of `Set.range f`. Then `f x` tends to `𝓝 a`
as `x → -∞` (formally, at the filter `Filter.atBot`). We require this for `ι = (s : Set α)`,
`f = (↑)` in the definition, then prove it for any `f` in `tendsto_atBot_isGLB`.

This property holds for linear orders with order topology as well as their products. -/
class InfConvergenceClass (α : Type*) [Preorder α] [TopologicalSpace α] : Prop where
  /-- proof that a monotone function tends to `𝓝 a` as `x → -∞` -/
  tendsto_coe_atBot_isGLB :
    ∀ (a : α) (s : Set α), IsGLB s a → Tendsto ((↑) : s → α) atBot (𝓝 a)
Inf-Convergence Class
Informal description
A type `α` with a preorder and topological space structure is said to be an `InfConvergenceClass` if the following property holds: For any monotone function `f : ι → α` with a greatest lower bound `a` of its range, the function `f` tends to `a` as `x → -∞` (i.e., along the filter `Filter.atBot`). This property is initially required for the inclusion map `(↑) : s → α` where `s` is a subset of `α`, and then generalized to any monotone function `f`. This property is satisfied by linear orders with their order topologies and their products.
OrderDual.supConvergenceClass instance
[Preorder α] [TopologicalSpace α] [InfConvergenceClass α] : SupConvergenceClass αᵒᵈ
Full source 
instance OrderDual.supConvergenceClass [Preorder α] [TopologicalSpace α] [InfConvergenceClass α] :
    SupConvergenceClass αᵒᵈ :=
  ⟨‹InfConvergenceClass α›.1⟩
Order Dual of an Inf-Convergence Class is a Sup-Convergence Class
Informal description
For any preordered topological space $\alpha$ that is an inf-convergence class, its order dual $\alpha^\mathrm{op}$ is a sup-convergence class. This means that in the order dual space, any monotone function with a least upper bound converges to that bound as the input tends to infinity.
OrderDual.infConvergenceClass instance
[Preorder α] [TopologicalSpace α] [SupConvergenceClass α] : InfConvergenceClass αᵒᵈ
Full source 
instance OrderDual.infConvergenceClass [Preorder α] [TopologicalSpace α] [SupConvergenceClass α] :
    InfConvergenceClass αᵒᵈ :=
  ⟨‹SupConvergenceClass α›.1⟩
Order Dual of a Sup-Convergence Class is an Inf-Convergence Class
Informal description
For any preorder $\alpha$ with a topological space structure, if $\alpha$ is a sup-convergence class, then its order dual $\alpha^\mathrm{op}$ is an inf-convergence class. This means that for any monotone function $f : \iota \to \alpha^\mathrm{op}$ with a greatest lower bound $a$ of its range, $f$ tends to $a$ as $x \to -\infty$ (i.e., along the filter $\mathrm{atBot}$).
LinearOrder.supConvergenceClass instance
[TopologicalSpace α] [LinearOrder α] [OrderTopology α] : SupConvergenceClass α
Full source 
instance (priority := 100) LinearOrder.supConvergenceClass [TopologicalSpace α] [LinearOrder α]
    [OrderTopology α] : SupConvergenceClass α := by
  refine ⟨fun a s ha => tendsto_order.2 ⟨fun b hb => ?_, fun b hb => ?_⟩⟩
  · rcases ha.exists_between hb with ⟨c, hcs, bc, bca⟩
    lift c to s using hcs
    exact (eventually_ge_atTop c).mono fun x hx => bc.trans_le hx
  · exact Eventually.of_forall fun x => (ha.1 x.2).trans_lt hb
Linear Orders with Order Topology are Sup-Convergence Classes
Informal description
Every linearly ordered topological space $\alpha$ with the order topology is a sup-convergence class. That is, for any monotone function $f : \iota \to \alpha$ with a least upper bound $a$ of its range, $f$ tends to $a$ as the input tends to infinity.
LinearOrder.infConvergenceClass instance
[TopologicalSpace α] [LinearOrder α] [OrderTopology α] : InfConvergenceClass α
Full source 
instance (priority := 100) LinearOrder.infConvergenceClass [TopologicalSpace α] [LinearOrder α]
    [OrderTopology α] : InfConvergenceClass α :=
  show InfConvergenceClass αᵒᵈαᵒᵈᵒᵈ from OrderDual.infConvergenceClass
Linear Orders with Order Topology are Inf-Convergence Classes
Informal description
Every linearly ordered topological space $\alpha$ with the order topology is an inf-convergence class. That is, for any monotone function $f : \iota \to \alpha$ with a greatest lower bound $a$ of its range, $f$ tends to $a$ as the input tends to negative infinity (i.e., along the filter $\mathrm{atBot}$).
tendsto_atTop_isLUB theorem
(h_mono : Monotone f) (ha : IsLUB (Set.range f) a) : Tendsto f atTop (𝓝 a)
Full source 
theorem tendsto_atTop_isLUB (h_mono : Monotone f) (ha : IsLUB (Set.range f) a) :
    Tendsto f atTop (𝓝 a) := by
  suffices Tendsto (rangeFactorization f) atTop atTop from
    (SupConvergenceClass.tendsto_coe_atTop_isLUB _ _ ha).comp this
  exact h_mono.rangeFactorization.tendsto_atTop_atTop fun b => b.2.imp fun a ha => ha.ge
Monotone Convergence Theorem: Tendency to Supremum at Infinity
Informal description
Let $f : \iota \to \alpha$ be a monotone function, where $\alpha$ is a preordered topological space. If $a$ is the least upper bound of the range of $f$, then $f$ tends to $a$ as the input tends to infinity (i.e., along the filter $\text{atTop}$).
tendsto_atBot_isLUB theorem
(h_anti : Antitone f) (ha : IsLUB (Set.range f) a) : Tendsto f atBot (𝓝 a)
Full source 
theorem tendsto_atBot_isLUB (h_anti : Antitone f) (ha : IsLUB (Set.range f) a) :
    Tendsto f atBot (𝓝 a) := by convert tendsto_atTop_isLUB h_anti.dual_left ha using 1
Antitone Convergence to Supremum at Negative Infinity
Informal description
Let $f : \iota \to \alpha$ be an antitone function, where $\alpha$ is a preordered topological space. If $a$ is the least upper bound of the range of $f$, then $f$ tends to $a$ as the input tends to negative infinity (i.e., along the filter $\text{atBot}$).
tendsto_atBot_isGLB theorem
(h_mono : Monotone f) (ha : IsGLB (Set.range f) a) : Tendsto f atBot (𝓝 a)
Full source 
theorem tendsto_atBot_isGLB (h_mono : Monotone f) (ha : IsGLB (Set.range f) a) :
    Tendsto f atBot (𝓝 a) := by convert tendsto_atTop_isLUB h_mono.dual ha.dual using 1
Monotone Convergence to Infimum at Negative Infinity
Informal description
Let $f : \iota \to \alpha$ be a monotone function, where $\alpha$ is a preordered topological space. If $a$ is the greatest lower bound of the range of $f$, then $f$ tends to $a$ as the input tends to negative infinity (i.e., along the filter $\text{atBot}$).
tendsto_atTop_isGLB theorem
(h_anti : Antitone f) (ha : IsGLB (Set.range f) a) : Tendsto f atTop (𝓝 a)
Full source 
theorem tendsto_atTop_isGLB (h_anti : Antitone f) (ha : IsGLB (Set.range f) a) :
    Tendsto f atTop (𝓝 a) := by convert tendsto_atBot_isLUB h_anti.dual ha.dual using 1
Antitone Convergence to Infimum at Infinity
Informal description
Let $\alpha$ be a preordered topological space and $f : \iota \to \alpha$ be an antitone function. If $a$ is the greatest lower bound of the range of $f$, then $f$ tends to $a$ as the index tends to infinity (i.e., along the filter $\text{atTop}$).
tendsto_atTop_ciSup theorem
(h_mono : Monotone f) (hbdd : BddAbove <| range f) : Tendsto f atTop (𝓝 (⨆ i, f i))
Full source 
theorem tendsto_atTop_ciSup (h_mono : Monotone f) (hbdd : BddAbove <| range f) :
    Tendsto f atTop (𝓝 (⨆ i, f i)) := by
  cases isEmpty_or_nonempty ι
  exacts [tendsto_of_isEmpty, tendsto_atTop_isLUB h_mono (isLUB_ciSup hbdd)]
Monotone Convergence to Indexed Supremum at Infinity
Informal description
Let $f : \iota \to \alpha$ be a monotone function in a conditionally complete lattice $\alpha$ with a topological space structure. If the range of $f$ is bounded above, then $f$ tends to its supremum $\bigsqcup_{i} f(i)$ as the index tends to infinity (i.e., along the filter $\text{atTop}$).
tendsto_atBot_ciSup theorem
(h_anti : Antitone f) (hbdd : BddAbove <| range f) : Tendsto f atBot (𝓝 (⨆ i, f i))
Full source 
theorem tendsto_atBot_ciSup (h_anti : Antitone f) (hbdd : BddAbove <| range f) :
    Tendsto f atBot (𝓝 (⨆ i, f i)) := by convert tendsto_atTop_ciSup h_anti.dual hbdd.dual using 1
Antitone Convergence to Indexed Supremum at Negative Infinity
Informal description
Let $\alpha$ be a conditionally complete lattice with a topological space structure, and let $f : \iota \to \alpha$ be an antitone function. If the range of $f$ is bounded above, then $f$ tends to its supremum $\bigsqcup_{i} f(i)$ as the index tends to negative infinity (i.e., along the filter $\text{atBot}$).
tendsto_atBot_ciInf theorem
(h_mono : Monotone f) (hbdd : BddBelow <| range f) : Tendsto f atBot (𝓝 (⨅ i, f i))
Full source 
theorem tendsto_atBot_ciInf (h_mono : Monotone f) (hbdd : BddBelow <| range f) :
    Tendsto f atBot (𝓝 (⨅ i, f i)) := by convert tendsto_atTop_ciSup h_mono.dual hbdd.dual using 1
Monotone Convergence to Indexed Infimum at Negative Infinity
Informal description
Let $\alpha$ be a conditionally complete lattice with a topological space structure, and let $f : \iota \to \alpha$ be a monotone function. If the range of $f$ is bounded below, then $f$ tends to its infimum $\bigsqcap_{i} f(i)$ as the index tends to negative infinity (i.e., along the filter $\text{atBot}$).
tendsto_atTop_ciInf theorem
(h_anti : Antitone f) (hbdd : BddBelow <| range f) : Tendsto f atTop (𝓝 (⨅ i, f i))
Full source 
theorem tendsto_atTop_ciInf (h_anti : Antitone f) (hbdd : BddBelow <| range f) :
    Tendsto f atTop (𝓝 (⨅ i, f i)) := by convert tendsto_atBot_ciSup h_anti.dual hbdd.dual using 1
Antitone Convergence to Indexed Infimum at Infinity
Informal description
Let $\alpha$ be a conditionally complete lattice with a topological space structure, and let $f : \iota \to \alpha$ be an antitone function. If the range of $f$ is bounded below, then $f$ tends to its infimum $\bigsqcap_{i} f(i)$ as the index tends to infinity (i.e., along the filter $\text{atTop}$).
tendsto_atTop_iSup theorem
(h_mono : Monotone f) : Tendsto f atTop (𝓝 (⨆ i, f i))
Full source 
theorem tendsto_atTop_iSup (h_mono : Monotone f) : Tendsto f atTop (𝓝 (⨆ i, f i)) :=
  tendsto_atTop_ciSup h_mono (OrderTop.bddAbove _)
Monotone Convergence to Supremum at Infinity
Informal description
Let $f : \iota \to \alpha$ be a monotone function in a complete lattice $\alpha$ with a topological space structure. Then $f$ tends to its supremum $\bigsqcup_{i} f(i)$ as the index tends to infinity (i.e., along the filter $\text{atTop}$).
tendsto_atBot_iSup theorem
(h_anti : Antitone f) : Tendsto f atBot (𝓝 (⨆ i, f i))
Full source 
theorem tendsto_atBot_iSup (h_anti : Antitone f) : Tendsto f atBot (𝓝 (⨆ i, f i)) :=
  tendsto_atBot_ciSup h_anti (OrderTop.bddAbove _)
Antitone Convergence to Supremum at Negative Infinity
Informal description
Let $\alpha$ be a complete lattice with a topological space structure, and let $f : \iota \to \alpha$ be an antitone function. Then $f$ tends to its supremum $\bigsqcup_{i} f(i)$ as the index tends to negative infinity (i.e., along the filter $\text{atBot}$).
tendsto_atBot_iInf theorem
(h_mono : Monotone f) : Tendsto f atBot (𝓝 (⨅ i, f i))
Full source 
theorem tendsto_atBot_iInf (h_mono : Monotone f) : Tendsto f atBot (𝓝 (⨅ i, f i)) :=
  tendsto_atBot_ciInf h_mono (OrderBot.bddBelow _)
Monotone Convergence to Infimum at Negative Infinity
Informal description
Let $\alpha$ be a complete lattice with a topological space structure, and let $f : \iota \to \alpha$ be a monotone function. Then $f$ tends to its infimum $\bigsqcap_{i} f(i)$ as the index tends to negative infinity (i.e., along the filter $\text{atBot}$).
tendsto_atTop_iInf theorem
(h_anti : Antitone f) : Tendsto f atTop (𝓝 (⨅ i, f i))
Full source 
theorem tendsto_atTop_iInf (h_anti : Antitone f) : Tendsto f atTop (𝓝 (⨅ i, f i)) :=
  tendsto_atTop_ciInf h_anti (OrderBot.bddBelow _)
Antitone Convergence to Infimum at Infinity
Informal description
Let $\alpha$ be a complete lattice with a topological space structure, and let $f : \iota \to \alpha$ be an antitone function. Then $f$ tends to its infimum $\bigsqcap_{i} f(i)$ as the index tends to infinity (i.e., along the filter $\mathrm{atTop}$).
Prod.supConvergenceClass instance
[Preorder α] [Preorder β] [TopologicalSpace α] [TopologicalSpace β] [SupConvergenceClass α] [SupConvergenceClass β] : SupConvergenceClass (α × β)
Full source 
instance Prod.supConvergenceClass
    [Preorder α] [Preorder β] [TopologicalSpace α] [TopologicalSpace β]
    [SupConvergenceClass α] [SupConvergenceClass β] : SupConvergenceClass (α × β) := by
  constructor
  rintro ⟨a, b⟩ s h
  rw [isLUB_prod, ← range_restrict, ← range_restrict] at h
  have A : Tendsto (fun x : s => (x : α × β).1) atTop (𝓝 a) :=
    tendsto_atTop_isLUB (monotone_fst.restrict s) h.1
  have B : Tendsto (fun x : s => (x : α × β).2) atTop (𝓝 b) :=
    tendsto_atTop_isLUB (monotone_snd.restrict s) h.2
  exact A.prodMk_nhds B
Product of Sup-Convergence Classes is a Sup-Convergence Class
Informal description
For any two preordered topological spaces $\alpha$ and $\beta$ that are sup-convergence classes, their product $\alpha \times \beta$ is also a sup-convergence class. This means that for any monotone function $f : \iota \to \alpha \times \beta$ with a least upper bound $(a, b)$ of its range, the function $f$ tends to $(a, b)$ as the input tends to infinity.
instInfConvergenceClassProd instance
[Preorder α] [Preorder β] [TopologicalSpace α] [TopologicalSpace β] [InfConvergenceClass α] [InfConvergenceClass β] : InfConvergenceClass (α × β)
Full source 
instance [Preorder α] [Preorder β] [TopologicalSpace α] [TopologicalSpace β] [InfConvergenceClass α]
    [InfConvergenceClass β] : InfConvergenceClass (α × β) :=
  show InfConvergenceClass (αᵒᵈ × βᵒᵈ)ᵒᵈ from OrderDual.infConvergenceClass
Product of Inf-Convergence Classes is an Inf-Convergence Class
Informal description
For any two preordered topological spaces $\alpha$ and $\beta$ that are inf-convergence classes, their product $\alpha \times \beta$ is also an inf-convergence class. This means that for any monotone function $f : \iota \to \alpha \times \beta$ with a greatest lower bound $(a, b)$ of its range, the function $f$ tends to $(a, b)$ as the input tends to $-\infty$ (i.e., along the filter $\mathrm{atBot}$).
Pi.supConvergenceClass instance
{ι : Type*} {α : ι → Type*} [∀ i, Preorder (α i)] [∀ i, TopologicalSpace (α i)] [∀ i, SupConvergenceClass (α i)] : SupConvergenceClass (∀ i, α i)
Full source 
instance Pi.supConvergenceClass
    {ι : Type*} {α : ι → Type*} [∀ i, Preorder (α i)] [∀ i, TopologicalSpace (α i)]
    [∀ i, SupConvergenceClass (α i)] : SupConvergenceClass (∀ i, α i) := by
  refine ⟨fun f s h => ?_⟩
  simp only [isLUB_pi, ← range_restrict] at h
  exact tendsto_pi_nhds.2 fun i => tendsto_atTop_isLUB ((monotone_eval _).restrict _) (h i)
Product of Sup-Convergence Classes is a Sup-Convergence Class
Informal description
For any family of preordered topological spaces $\{\alpha_i\}_{i \in \iota}$ where each $\alpha_i$ is a sup-convergence class, the product space $\prod_{i \in \iota} \alpha_i$ is also a sup-convergence class. This means that for any monotone function $f : \kappa \to \prod_{i \in \iota} \alpha_i$ with a least upper bound $a$ of its range, the function $f$ tends to $a$ as the input tends to infinity.
Pi.infConvergenceClass instance
{ι : Type*} {α : ι → Type*} [∀ i, Preorder (α i)] [∀ i, TopologicalSpace (α i)] [∀ i, InfConvergenceClass (α i)] : InfConvergenceClass (∀ i, α i)
Full source 
instance Pi.infConvergenceClass
    {ι : Type*} {α : ι → Type*} [∀ i, Preorder (α i)] [∀ i, TopologicalSpace (α i)]
    [∀ i, InfConvergenceClass (α i)] : InfConvergenceClass (∀ i, α i) :=
  show InfConvergenceClass (∀ i, (α i)ᵒᵈ)ᵒᵈ from OrderDual.infConvergenceClass
Product of Inf-Convergence Classes is an Inf-Convergence Class
Informal description
For any family of preordered topological spaces $\{\alpha_i\}_{i \in \iota}$ where each $\alpha_i$ is an inf-convergence class, the product space $\prod_{i \in \iota} \alpha_i$ is also an inf-convergence class. This means that for any monotone function $f : \kappa \to \prod_{i \in \iota} \alpha_i$ with a greatest lower bound $(a_i)_{i \in \iota}$ of its range, the function $f$ tends to $(a_i)_{i \in \iota}$ as the input tends to $-\infty$ (i.e., along the filter $\mathrm{atBot}$).
Pi.supConvergenceClass' instance
{ι : Type*} [Preorder α] [TopologicalSpace α] [SupConvergenceClass α] : SupConvergenceClass (ι → α)
Full source 
instance Pi.supConvergenceClass' {ι : Type*} [Preorder α] [TopologicalSpace α]
    [SupConvergenceClass α] : SupConvergenceClass (ι → α) :=
  supConvergenceClass
Function Space of Sup-Convergence Classes is a Sup-Convergence Class
Informal description
For any preordered topological space $\alpha$ that is a sup-convergence class, the function space $\iota \to \alpha$ (with pointwise order and topology) is also a sup-convergence class. This means that for any monotone function $f : \kappa \to (\iota \to \alpha)$ with a least upper bound $a$ of its range, the function $f$ tends to $a$ as the input tends to infinity.
Pi.infConvergenceClass' instance
{ι : Type*} [Preorder α] [TopologicalSpace α] [InfConvergenceClass α] : InfConvergenceClass (ι → α)
Full source 
instance Pi.infConvergenceClass' {ι : Type*} [Preorder α] [TopologicalSpace α]
    [InfConvergenceClass α] : InfConvergenceClass (ι → α) :=
  Pi.infConvergenceClass
Function Space of Inf-Convergence Classes is an Inf-Convergence Class
Informal description
For any preordered topological space $\alpha$ that is an inf-convergence class, the function space $\iota \to \alpha$ (with pointwise order and topology) is also an inf-convergence class. This means that for any monotone function $f : \kappa \to (\iota \to \alpha)$ with a greatest lower bound $a$ of its range, the function $f$ tends to $a$ as the input tends to $-\infty$ (i.e., along the filter $\mathrm{atBot}$).
tendsto_of_monotone theorem
{ι α : Type*} [Preorder ι] [TopologicalSpace α] [ConditionallyCompleteLinearOrder α] [OrderTopology α] {f : ι → α} (h_mono : Monotone f) : Tendsto f atTop atTop ∨ ∃ l, Tendsto f atTop (𝓝 l)
Full source 
theorem tendsto_of_monotone {ι α : Type*} [Preorder ι] [TopologicalSpace α]
    [ConditionallyCompleteLinearOrder α] [OrderTopology α] {f : ι → α} (h_mono : Monotone f) :
    TendstoTendsto f atTop atTop ∨ ∃ l, Tendsto f atTop (𝓝 l) := by
  classical
  exact if H : BddAbove (range f) then Or.inr ⟨_, tendsto_atTop_ciSup h_mono H⟩
  else Or.inl <| tendsto_atTop_atTop_of_monotone' h_mono H
Monotone Functions Tend to Infinity or a Finite Limit in Conditionally Complete Linear Orders
Informal description
Let $\alpha$ be a conditionally complete linear order with the order topology, and let $f : \iota \to \alpha$ be a monotone function defined on a preordered set $\iota$. Then either $f$ tends to infinity (i.e., $\lim_{x \to \infty} f(x) = \infty$) or there exists a limit $l \in \alpha$ such that $f$ tends to $l$ as $x \to \infty$.
tendsto_of_antitone theorem
{ι α : Type*} [Preorder ι] [TopologicalSpace α] [ConditionallyCompleteLinearOrder α] [OrderTopology α] {f : ι → α} (h_mono : Antitone f) : Tendsto f atTop atBot ∨ ∃ l, Tendsto f atTop (𝓝 l)
Full source 
theorem tendsto_of_antitone {ι α : Type*} [Preorder ι] [TopologicalSpace α]
    [ConditionallyCompleteLinearOrder α] [OrderTopology α] {f : ι → α} (h_mono : Antitone f) :
    TendstoTendsto f atTop atBot ∨ ∃ l, Tendsto f atTop (𝓝 l) :=
  @tendsto_of_monotone ι αᵒᵈ _ _ _ _ _ h_mono
Antitone Functions Tend to Negative Infinity or a Finite Limit in Conditionally Complete Linear Orders
Informal description
Let $\alpha$ be a conditionally complete linear order with the order topology, and let $f : \iota \to \alpha$ be an antitone function defined on a preordered set $\iota$. Then either $f$ tends to negative infinity (i.e., $\lim_{x \to \infty} f(x) = -\infty$) or there exists a limit $l \in \alpha$ such that $f$ tends to $l$ as $x \to \infty$.
tendsto_iff_tendsto_subseq_of_monotone theorem
{ι₁ ι₂ α : Type*} [SemilatticeSup ι₁] [Preorder ι₂] [Nonempty ι₁] [TopologicalSpace α] [ConditionallyCompleteLinearOrder α] [OrderTopology α] [NoMaxOrder α] {f : ι₂ → α} {φ : ι₁ → ι₂} {l : α} (hf : Monotone f) (hg : Tendsto φ atTop atTop) : Tendsto f atTop (𝓝 l) ↔ Tendsto (f ∘ φ) atTop (𝓝 l)
Full source 
theorem tendsto_iff_tendsto_subseq_of_monotone {ι₁ ι₂ α : Type*} [SemilatticeSup ι₁] [Preorder ι₂]
    [Nonempty ι₁] [TopologicalSpace α] [ConditionallyCompleteLinearOrder α] [OrderTopology α]
    [NoMaxOrder α] {f : ι₂ → α} {φ : ι₁ → ι₂} {l : α} (hf : Monotone f)
    (hg : Tendsto φ atTop atTop) : TendstoTendsto f atTop (𝓝 l) ↔ Tendsto (f ∘ φ) atTop (𝓝 l) := by
  constructor <;> intro h
  · exact h.comp hg
  · rcases tendsto_of_monotone hf with (h' | ⟨l', hl'⟩)
    · exact (not_tendsto_atTop_of_tendsto_nhds h (h'.comp hg)).elim
    · rwa [tendsto_nhds_unique h (hl'.comp hg)]
Monotone Function Limit via Subsequence in Conditionally Complete Linear Order
Informal description
Let $\alpha$ be a conditionally complete linear order with the order topology and no maximal element, and let $\iota_1$ be a nonempty semilattice with a supremum operation and $\iota_2$ be a preordered set. Given a monotone function $f \colon \iota_2 \to \alpha$, a sequence $\varphi \colon \iota_1 \to \iota_2$ that tends to infinity, and a point $l \in \alpha$, the following are equivalent: 1. The function $f$ tends to $l$ as $x \to \infty$ in $\iota_2$. 2. The composition $f \circ \varphi$ tends to $l$ as $n \to \infty$ in $\iota_1$.
tendsto_iff_tendsto_subseq_of_antitone theorem
{ι₁ ι₂ α : 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)
Full source 
theorem tendsto_iff_tendsto_subseq_of_antitone {ι₁ ι₂ α : Type*} [SemilatticeSup ι₁] [Preorder ι₂]
    [Nonempty ι₁] [TopologicalSpace α] [ConditionallyCompleteLinearOrder α] [OrderTopology α]
    [NoMinOrder α] {f : ι₂ → α} {φ : ι₁ → ι₂} {l : α} (hf : Antitone f)
    (hg : Tendsto φ atTop atTop) : TendstoTendsto f atTop (𝓝 l) ↔ Tendsto (f ∘ φ) atTop (𝓝 l) :=
  tendsto_iff_tendsto_subseq_of_monotone (α := αᵒᵈ) hf hg
Antitone Function Limit via Subsequence in Conditionally Complete Linear Order
Informal description
Let $\alpha$ be a conditionally complete linear order with the order topology and no minimal element, and let $\iota_1$ be a nonempty semilattice with a supremum operation and $\iota_2$ be a preordered set. Given an antitone function $f \colon \iota_2 \to \alpha$, a sequence $\varphi \colon \iota_1 \to \iota_2$ that tends to infinity, and a point $l \in \alpha$, the following are equivalent: 1. The function $f$ tends to $l$ as $x \to \infty$ in $\iota_2$. 2. The composition $f \circ \varphi$ tends to $l$ as $n \to \infty$ in $\iota_1$.
Monotone.ge_of_tendsto theorem
[TopologicalSpace α] [Preorder α] [OrderClosedTopology α] [SemilatticeSup β] {f : β → α} {a : α} (hf : Monotone f) (ha : Tendsto f atTop (𝓝 a)) (b : β) : f b ≤ a
Full source 
theorem Monotone.ge_of_tendsto [TopologicalSpace α] [Preorder α] [OrderClosedTopology α]
    [SemilatticeSup β] {f : β → α} {a : α} (hf : Monotone f) (ha : Tendsto f atTop (𝓝 a)) (b : β) :
    f b ≤ a :=
  haveI : Nonempty β := Nonempty.intro b
  _root_.ge_of_tendsto ha ((eventually_ge_atTop b).mono fun _ hxy => hf hxy)
Monotone Sequence Upper Bound: $f(b) \leq \lim f$
Informal description
Let $\alpha$ be a topological space with a preorder and order-closed topology, and let $\beta$ be a semilattice with a supremum operation. Given a monotone function $f \colon \beta \to \alpha$ and a point $a \in \alpha$ such that $f$ tends to $a$ along the filter at infinity, then for any $b \in \beta$, we have $f(b) \leq a$.
Monotone.le_of_tendsto theorem
[TopologicalSpace α] [Preorder α] [OrderClosedTopology α] [SemilatticeInf β] {f : β → α} {a : α} (hf : Monotone f) (ha : Tendsto f atBot (𝓝 a)) (b : β) : a ≤ f b
Full source 
theorem Monotone.le_of_tendsto [TopologicalSpace α] [Preorder α] [OrderClosedTopology α]
    [SemilatticeInf β] {f : β → α} {a : α} (hf : Monotone f) (ha : Tendsto f atBot (𝓝 a)) (b : β) :
    a ≤ f b :=
  hf.dual.ge_of_tendsto ha b
Monotone Sequence Lower Bound: $\lim f \leq f(b)$
Informal description
Let $\alpha$ be a topological space with a preorder and order-closed topology, and let $\beta$ be a semilattice with an infimum operation. Given a monotone function $f \colon \beta \to \alpha$ and a point $a \in \alpha$ such that $f$ tends to $a$ along the filter at negative infinity, then for any $b \in \beta$, we have $a \leq f(b)$.
Antitone.le_of_tendsto theorem
[TopologicalSpace α] [Preorder α] [OrderClosedTopology α] [SemilatticeSup β] {f : β → α} {a : α} (hf : Antitone f) (ha : Tendsto f atTop (𝓝 a)) (b : β) : a ≤ f b
Full source 
theorem Antitone.le_of_tendsto [TopologicalSpace α] [Preorder α] [OrderClosedTopology α]
    [SemilatticeSup β] {f : β → α} {a : α} (hf : Antitone f) (ha : Tendsto f atTop (𝓝 a)) (b : β) :
    a ≤ f b :=
  hf.dual_right.ge_of_tendsto ha b
Antitone Sequence Lower Bound: $\lim f \leq f(b)$ at $\infty$
Informal description
Let $\alpha$ be a topological space with a preorder and order-closed topology, and let $\beta$ be a semilattice with a supremum operation. Given an antitone function $f \colon \beta \to \alpha$ and a point $a \in \alpha$ such that $f$ tends to $a$ along the filter at infinity, then for any $b \in \beta$, we have $a \leq f(b)$.
Antitone.ge_of_tendsto theorem
[TopologicalSpace α] [Preorder α] [OrderClosedTopology α] [SemilatticeInf β] {f : β → α} {a : α} (hf : Antitone f) (ha : Tendsto f atBot (𝓝 a)) (b : β) : f b ≤ a
Full source 
theorem Antitone.ge_of_tendsto [TopologicalSpace α] [Preorder α] [OrderClosedTopology α]
    [SemilatticeInf β] {f : β → α} {a : α} (hf : Antitone f) (ha : Tendsto f atBot (𝓝 a)) (b : β) :
    f b ≤ a :=
  hf.dual_right.le_of_tendsto ha b
Antitone Sequence Upper Bound: $f(b) \leq \lim f$ at $-\infty$
Informal description
Let $\alpha$ be a topological space with a preorder and order-closed topology, and let $\beta$ be a semilattice with an infimum operation. Given an antitone function $f \colon \beta \to \alpha$ and a point $a \in \alpha$ such that $f$ tends to $a$ along the filter at negative infinity, then for any $b \in \beta$, we have $f(b) \leq a$.
isLUB_of_tendsto_atTop theorem
[TopologicalSpace α] [Preorder α] [OrderClosedTopology α] [Nonempty β] [SemilatticeSup β] {f : β → α} {a : α} (hf : Monotone f) (ha : Tendsto f atTop (𝓝 a)) : IsLUB (Set.range f) a
Full source 
theorem isLUB_of_tendsto_atTop [TopologicalSpace α] [Preorder α] [OrderClosedTopology α]
    [Nonempty β] [SemilatticeSup β] {f : β → α} {a : α} (hf : Monotone f)
    (ha : Tendsto f atTop (𝓝 a)) : IsLUB (Set.range f) a := by
  constructor
  · rintro _ ⟨b, rfl⟩
    exact hf.ge_of_tendsto ha b
  · exact fun _ hb => le_of_tendsto' ha fun x => hb (Set.mem_range_self x)
Least Upper Bound of Monotone Sequence at Infinity
Informal description
Let $\alpha$ be a topological space with a preorder and order-closed topology, and let $\beta$ be a nonempty semilattice with a supremum operation. Given a monotone function $f \colon \beta \to \alpha$ and a point $a \in \alpha$ such that $f$ tends to $a$ along the filter at infinity, then $a$ is the least upper bound of the range of $f$.
isGLB_of_tendsto_atBot theorem
[TopologicalSpace α] [Preorder α] [OrderClosedTopology α] [Nonempty β] [SemilatticeInf β] {f : β → α} {a : α} (hf : Monotone f) (ha : Tendsto f atBot (𝓝 a)) : IsGLB (Set.range f) a
Full source 
theorem isGLB_of_tendsto_atBot [TopologicalSpace α] [Preorder α] [OrderClosedTopology α]
    [Nonempty β] [SemilatticeInf β] {f : β → α} {a : α} (hf : Monotone f)
    (ha : Tendsto f atBot (𝓝 a)) : IsGLB (Set.range f) a :=
  @isLUB_of_tendsto_atTop αᵒᵈ βᵒᵈ _ _ _ _ _ _ _ hf.dual ha
Greatest Lower Bound of Monotone Sequence at Negative Infinity
Informal description
Let $\alpha$ be a topological space with a preorder and order-closed topology, and let $\beta$ be a nonempty semilattice with an infimum operation. Given a monotone function $f \colon \beta \to \alpha$ and a point $a \in \alpha$ such that $f$ tends to $a$ along the filter at negative infinity, then $a$ is the greatest lower bound of the range of $f$.
isLUB_of_tendsto_atBot theorem
[TopologicalSpace α] [Preorder α] [OrderClosedTopology α] [Nonempty β] [SemilatticeInf β] {f : β → α} {a : α} (hf : Antitone f) (ha : Tendsto f atBot (𝓝 a)) : IsLUB (Set.range f) a
Full source 
theorem isLUB_of_tendsto_atBot [TopologicalSpace α] [Preorder α] [OrderClosedTopology α]
    [Nonempty β] [SemilatticeInf β] {f : β → α} {a : α} (hf : Antitone f)
    (ha : Tendsto f atBot (𝓝 a)) : IsLUB (Set.range f) a :=
  @isLUB_of_tendsto_atTop α βᵒᵈ _ _ _ _ _ _ _ hf.dual_left ha
Least Upper Bound of Antitone Sequence at Negative Infinity
Informal description
Let $\alpha$ be a topological space with a preorder and order-closed topology, and let $\beta$ be a nonempty semilattice with an infimum operation. Given an antitone function $f \colon \beta \to \alpha$ and a point $a \in \alpha$ such that $f$ tends to $a$ along the filter at negative infinity, then $a$ is the least upper bound of the range of $f$.
isGLB_of_tendsto_atTop theorem
[TopologicalSpace α] [Preorder α] [OrderClosedTopology α] [Nonempty β] [SemilatticeSup β] {f : β → α} {a : α} (hf : Antitone f) (ha : Tendsto f atTop (𝓝 a)) : IsGLB (Set.range f) a
Full source 
theorem isGLB_of_tendsto_atTop [TopologicalSpace α] [Preorder α] [OrderClosedTopology α]
    [Nonempty β] [SemilatticeSup β] {f : β → α} {a : α} (hf : Antitone f)
    (ha : Tendsto f atTop (𝓝 a)) : IsGLB (Set.range f) a :=
  @isGLB_of_tendsto_atBot α βᵒᵈ _ _ _ _ _ _ _ hf.dual_left ha
Greatest Lower Bound of Antitone Sequence at Positive Infinity
Informal description
Let $\alpha$ be a topological space with a preorder and order-closed topology, and let $\beta$ be a nonempty semilattice with a supremum operation. Given an antitone function $f \colon \beta \to \alpha$ and a point $a \in \alpha$ such that $f$ tends to $a$ along the filter at positive infinity, then $a$ is the greatest lower bound of the range of $f$.
iSup_eq_of_tendsto theorem
{α β} [TopologicalSpace α] [CompleteLinearOrder α] [OrderTopology α] [Nonempty β] [SemilatticeSup β] {f : β → α} {a : α} (hf : Monotone f) : Tendsto f atTop (𝓝 a) → iSup f = a
Full source 
theorem iSup_eq_of_tendsto {α β} [TopologicalSpace α] [CompleteLinearOrder α] [OrderTopology α]
    [Nonempty β] [SemilatticeSup β] {f : β → α} {a : α} (hf : Monotone f) :
    Tendsto f atTop (𝓝 a) → iSup f = a :=
  tendsto_nhds_unique (tendsto_atTop_iSup hf)
Supremum of Monotone Sequence Equals Limit at Infinity
Informal description
Let $\alpha$ be a complete linear order with the order topology, and let $\beta$ be a nonempty semilattice with a supremum operation. Given a monotone function $f \colon \beta \to \alpha$ and a point $a \in \alpha$ such that $f$ tends to $a$ along the filter at infinity, then the supremum of $f$ is equal to $a$, i.e., \[ \bigsqcup_{i \in \beta} f(i) = a. \]
iInf_eq_of_tendsto theorem
{α} [TopologicalSpace α] [CompleteLinearOrder α] [OrderTopology α] [Nonempty β] [SemilatticeSup β] {f : β → α} {a : α} (hf : Antitone f) : Tendsto f atTop (𝓝 a) → iInf f = a
Full source 
theorem iInf_eq_of_tendsto {α} [TopologicalSpace α] [CompleteLinearOrder α] [OrderTopology α]
    [Nonempty β] [SemilatticeSup β] {f : β → α} {a : α} (hf : Antitone f) :
    Tendsto f atTop (𝓝 a) → iInf f = a :=
  tendsto_nhds_unique (tendsto_atTop_iInf hf)
Infimum of Antitone Sequence Equals Limit at Infinity
Informal description
Let $\alpha$ be a complete linear order with the order topology, and let $\beta$ be a nonempty semilattice with a supremum operation. Given an antitone function $f \colon \beta \to \alpha$ and a point $a \in \alpha$ such that $f$ tends to $a$ along the filter at infinity, then the infimum of $f$ is equal to $a$, i.e., \[ \bigsqcap_{i \in \beta} f(i) = a. \]
iSup_eq_iSup_subseq_of_monotone theorem
{ι₁ ι₂ α : Type*} [Preorder ι₂] [CompleteLattice α] {l : Filter ι₁} [l.NeBot] {f : ι₂ → α} {φ : ι₁ → ι₂} (hf : Monotone f) (hφ : Tendsto φ l atTop) : ⨆ i, f i = ⨆ i, f (φ i)
Full source 
theorem iSup_eq_iSup_subseq_of_monotone {ι₁ ι₂ α : Type*} [Preorder ι₂] [CompleteLattice α]
    {l : Filter ι₁} [l.NeBot] {f : ι₂ → α} {φ : ι₁ → ι₂} (hf : Monotone f)
    (hφ : Tendsto φ l atTop) : ⨆ i, f i = ⨆ i, f (φ i) :=
  le_antisymm
    (iSup_mono' fun i =>
      Exists.imp (fun j (hj : i ≤ φ j) => hf hj) (hφ.eventually <| eventually_ge_atTop i).exists)
    (iSup_mono' fun i => ⟨φ i, le_rfl⟩)
Supremum Equality for Monotone Functions via Subsequences
Informal description
Let $\iota_1$ and $\iota_2$ be types with $\iota_2$ equipped with a preorder, and let $\alpha$ be a complete lattice. Consider a non-trivial filter $l$ on $\iota_1$, a monotone function $f : \iota_2 \to \alpha$, and a function $\varphi : \iota_1 \to \iota_2$ such that $\varphi$ tends to infinity along $l$. Then the supremum of $f$ over $\iota_2$ is equal to the supremum of $f \circ \varphi$ over $\iota_1$, i.e., \[ \bigsqcup_{i \in \iota_2} f(i) = \bigsqcup_{i \in \iota_1} f(\varphi(i)). \]
iSup_eq_iSup_subseq_of_antitone theorem
{ι₁ ι₂ α : Type*} [Preorder ι₂] [CompleteLattice α] {l : Filter ι₁} [l.NeBot] {f : ι₂ → α} {φ : ι₁ → ι₂} (hf : Antitone f) (hφ : Tendsto φ l atBot) : ⨆ i, f i = ⨆ i, f (φ i)
Full source 
theorem iSup_eq_iSup_subseq_of_antitone {ι₁ ι₂ α : Type*} [Preorder ι₂] [CompleteLattice α]
    {l : Filter ι₁} [l.NeBot] {f : ι₂ → α} {φ : ι₁ → ι₂} (hf : Antitone f)
    (hφ : Tendsto φ l atBot) : ⨆ i, f i = ⨆ i, f (φ i) :=
  le_antisymm
    (iSup_mono' fun i =>
      Exists.imp (fun j (hj : φ j ≤ i) => hf hj) (hφ.eventually <| eventually_le_atBot i).exists)
    (iSup_mono' fun i => ⟨φ i, le_rfl⟩)
Supremum Equality for Antitone Functions via Subsequences Tending to Negative Infinity
Informal description
Let $\iota_1$ and $\iota_2$ be types with $\iota_2$ equipped with a preorder, and let $\alpha$ be a complete lattice. Consider a non-trivial filter $l$ on $\iota_1$, an antitone function $f : \iota_2 \to \alpha$, and a function $\varphi : \iota_1 \to \iota_2$ such that $\varphi$ tends to negative infinity along $l$. Then the supremum of $f$ over $\iota_2$ is equal to the supremum of $f \circ \varphi$ over $\iota_1$, i.e., \[ \bigsqcup_{i \in \iota_2} f(i) = \bigsqcup_{i \in \iota_1} f(\varphi(i)). \]
iInf_eq_iInf_subseq_of_monotone theorem
{ι₁ ι₂ α : Type*} [Preorder ι₂] [CompleteLattice α] {l : Filter ι₁} [l.NeBot] {f : ι₂ → α} {φ : ι₁ → ι₂} (hf : Monotone f) (hφ : Tendsto φ l atBot) : ⨅ i, f i = ⨅ i, f (φ i)
Full source 
theorem iInf_eq_iInf_subseq_of_monotone {ι₁ ι₂ α : Type*} [Preorder ι₂] [CompleteLattice α]
    {l : Filter ι₁} [l.NeBot] {f : ι₂ → α} {φ : ι₁ → ι₂} (hf : Monotone f)
    (hφ : Tendsto φ l atBot) : ⨅ i, f i = ⨅ i, f (φ i) :=
  iSup_eq_iSup_subseq_of_monotone hf.dual hφ
Infimum Equality for Monotone Functions via Subsequences Tending to Negative Infinity
Informal description
Let $\iota_1$ and $\iota_2$ be types with $\iota_2$ equipped with a preorder, and let $\alpha$ be a complete lattice. Given a non-trivial filter $l$ on $\iota_1$, a monotone function $f : \iota_2 \to \alpha$, and a function $\varphi : \iota_1 \to \iota_2$ such that $\varphi$ tends to negative infinity along $l$, the infimum of $f$ over $\iota_2$ equals the infimum of $f \circ \varphi$ over $\iota_1$, i.e., \[ \bigsqcap_{i \in \iota_2} f(i) = \bigsqcap_{i \in \iota_1} f(\varphi(i)). \]
iInf_eq_iInf_subseq_of_antitone theorem
{ι₁ ι₂ α : Type*} [Preorder ι₂] [CompleteLattice α] {l : Filter ι₁} [l.NeBot] {f : ι₂ → α} {φ : ι₁ → ι₂} (hf : Antitone f) (hφ : Tendsto φ l atTop) : ⨅ i, f i = ⨅ i, f (φ i)
Full source 
theorem iInf_eq_iInf_subseq_of_antitone {ι₁ ι₂ α : Type*} [Preorder ι₂] [CompleteLattice α]
    {l : Filter ι₁} [l.NeBot] {f : ι₂ → α} {φ : ι₁ → ι₂} (hf : Antitone f)
    (hφ : Tendsto φ l atTop) : ⨅ i, f i = ⨅ i, f (φ i) :=
  iSup_eq_iSup_subseq_of_antitone hf.dual hφ
Infimum Equality for Antitone Functions via Subsequences Tending to Infinity
Informal description
Let $\iota_1$ and $\iota_2$ be types with $\iota_2$ equipped with a preorder, and let $\alpha$ be a complete lattice. Consider a non-trivial filter $l$ on $\iota_1$, an antitone function $f : \iota_2 \to \alpha$, and a function $\varphi : \iota_1 \to \iota_2$ such that $\varphi$ tends to infinity along $l$. Then the infimum of $f$ over $\iota_2$ is equal to the infimum of $f \circ \varphi$ over $\iota_1$, i.e., \[ \bigsqcap_{i \in \iota_2} f(i) = \bigsqcap_{i \in \iota_1} f(\varphi(i)). \]