iSup_eq_iSup_subseq_of_monotone
theorem iSup_eq_iSup_subseq_of_monotone :
∀ {ι₁ : Type u_3} {ι₂ : Type u_4} {α : Type u_5} [inst : Preorder ι₂] [inst_1 : CompleteLattice α] {l : Filter ι₁}
[inst_2 : l.NeBot] {f : ι₂ → α} {φ : ι₁ → ι₂},
Monotone f → Filter.Tendsto φ l Filter.atTop → ⨆ i, f i = ⨆ i, f (φ i)
This theorem states that for any types `ι₁`, `ι₂`, `α` and a function `f` from `ι₂` to `α` where `ι₂` has a preorder structure and `α` has a complete lattice structure, and a function `φ` from `ι₁` to `ι₂`, if `f` is a monotone function and `φ` tends to infinity with respect to some filter `l` on `ι₁` that is not `⊥` (the smallest filter or the empty set), then the supremum (`⨆`) of the values of `f` over all `ι₂` is equal to the supremum of the values of `f` composed with `φ` over all `ι₁`.
In simpler terms, if `f` is a function that preserves order, and `φ` is a function that generates a sequence that goes to infinity, then the largest value that `f` can take (when it is defined for all `ι₂`) is the same as the largest value that `f` can take when it is applied to the sequence generated by `φ`.
More concisely: If `f: ι₂ → α` is a monotone function, `φ: ι₁ → ι₂` is a function, `ι₂` is a preordered type with a complete lattice structure, `ι₁` is non-empty and has a filter `l` not equal to the bottom element, then `⨆ (f ∘ φ) (i₁ : ι₁) = ⨆ f (i₂ : ι₂)`.
|
tendsto_atTop_iSup
theorem tendsto_atTop_iSup :
∀ {α : Type u_1} {ι : Type u_3} [inst : Preorder ι] [inst_1 : TopologicalSpace α] [inst_2 : CompleteLattice α]
[inst_3 : SupConvergenceClass α] {f : ι → α}, Monotone f → Filter.Tendsto f Filter.atTop (nhds (⨆ i, f i))
The theorem `tendsto_atTop_iSup` states that for any types `α` and `ι`, where `α` has a topological space structure and is also a complete lattice, and `ι` is preordered, given a function `f` from `ι` to `α`, if `f` is monotone, then `f` tends to the supremum of `f` at `∞`. In other words, for every neighborhood of the supremum of `f`, the pre-image of that neighborhood under `f` contains all sufficiently large elements of `ι`.
More concisely: For any monotone function `f` from a preordered type `ι` to a complete lattice `α` with topological space structure, if `∞` is in `ι` and `f(∞)` is the supremum of `f` over `ι`, then for every neighborhood of `f(∞)` in `α`, the preimage `f⁻¹(U)` contains all `i` in `ι` such that `i` is larger than some element in `ι`.
|
isLUB_of_tendsto_atTop
theorem isLUB_of_tendsto_atTop :
∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : Preorder α] [inst_2 : OrderClosedTopology α]
[inst_3 : Nonempty β] [inst_4 : SemilatticeSup β] {f : β → α} {a : α},
Monotone f → Filter.Tendsto f Filter.atTop (nhds a) → IsLUB (Set.range f) a
The theorem `isLUB_of_tendsto_atTop` states that for any topological space `α` with a preorder and an order-closed topology, any nonempty semilattice `β`, a monotone function `f` from `β` to `α`, and an element `a` in `α`, if `f` tends to `a` as it approaches infinity (`Filter.Tendsto f Filter.atTop (nhds a)`), then `a` is a least upper bound (LUB) of the range of `f` (`IsLUB (Set.range f) a`).
In other words, if `f` is a monotone function whose limit at infinity is `a`, then `a` is the smallest value that is greater than or equal to all values in the range of `f`. This theorem is a combination of topology (concerning limits of functions) and order theory (concerning upper bounds).
More concisely: If `α` is a topological space with a preorder and an order-closed topology, `β` is a nonempty semilattice, `f` is a monotone function from `β` to `α`, and `a` is the limit of `f` as it approaches infinity, then `a` is the least upper bound of the range of `f`.
|
Monotone.le_of_tendsto
theorem Monotone.le_of_tendsto :
∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : Preorder α] [inst_2 : OrderClosedTopology α]
[inst_3 : SemilatticeInf β] {f : β → α} {a : α},
Monotone f → Filter.Tendsto f Filter.atBot (nhds a) → ∀ (b : β), a ≤ f b
This theorem states that if a function `f` from an ordered set `β` to a topological space `α` is monotone, and the limit of `f` as `β` approaches negative infinity is a point `a` in `α`, then for any element `b` in `β`, `a` will be less than or equal to `f(b)`. Here, `α` is equipped with a preorder and an order-closed topology, and `β` is assumed to be a semilattice with respect to the infimum operation.
More concisely: If `f` is a monotone function from the semilattice `β` with infimum operation to the ordered topological space `(α, ≤)`, and `a` is the limit of `f` as `β` approaches negative infinity, then `a ≤ f(b)` for all `b` in `β`.
|
tendsto_atTop_ciSup
theorem tendsto_atTop_ciSup :
∀ {α : Type u_1} {ι : Type u_3} [inst : Preorder ι] [inst_1 : TopologicalSpace α]
[inst_2 : ConditionallyCompleteLattice α] [inst_3 : SupConvergenceClass α] {f : ι → α},
Monotone f → BddAbove (Set.range f) → Filter.Tendsto f Filter.atTop (nhds (⨆ i, f i))
This theorem, named `tendsto_atTop_ciSup`, states that for any types `α` and `ι` where `α` has a topological space structure, is a conditionally complete lattice, and satisfies the supremum convergence class properties, and `ι` has a preorder structure, and given a function `f` from `ι` to `α` that is monotone and its range is bounded above, then the function `f` tends to the supremum of `f i` as `i` tends towards infinity. In other words, for any `α` in the supremum neighborhood, there exists an `i` such that for all `j` greater than or equal to `i`, `f(j)` is in `α`. The supremum here is the least upper bound of `f i` for all `i` in `ι`.
More concisely: Given a monotone function `f` from a preordered type `ι` to a topological space `α` with a conditionally complete lattice structure and supremum convergence properties, if the range of `f` is bounded above, then for any `α` in the supremum neighborhood, there exists an `i` such that for all `j ≥ i`, `f(j)` is in `α`, i.e., `f` converges to the supremum of `f(i)` as `i` approaches infinity.
|
tendsto_of_monotone
theorem tendsto_of_monotone :
∀ {ι : Type u_3} {α : Type u_4} [inst : Preorder ι] [inst_1 : TopologicalSpace α]
[inst_2 : ConditionallyCompleteLinearOrder α] [inst_3 : OrderTopology α] {f : ι → α},
Monotone f → Filter.Tendsto f Filter.atTop Filter.atTop ∨ ∃ l, Filter.Tendsto f Filter.atTop (nhds l)
This theorem, `tendsto_of_monotone`, states that for any type `ι` with a preorder and any type `α` with a topological space structure, a conditionally complete linear order and an order topology, if we have a function `f` from `ι` to `α` that is monotone, then either `f` tends to infinity as `ι` tends to infinity, or there exists a limit `l` such that `f` tends to `l` as `ι` tends to infinity. In mathematical terms, we could express it as: if $f$ is a monotone function, then $\lim_{x\to\infty} f(x) = \infty$ or $\lim_{x\to\infty} f(x) = l$ for some $l$ in the codomain.
More concisely: A monotone function from a preordered type with a topology to a type with a complete order topology either converges to infinity or has a limit.
|
InfConvergenceClass.tendsto_coe_atBot_isGLB
theorem InfConvergenceClass.tendsto_coe_atBot_isGLB :
∀ {α : Type u_3} [inst : Preorder α] [inst_1 : TopologicalSpace α] [self : InfConvergenceClass α] (a : α)
(s : Set α), IsGLB s a → Filter.Tendsto CoeTC.coe Filter.atBot (nhds a)
This theorem states that for any given type `α` with a preorder relation and a topology, and any set `s` of `α` with a greatest lower bound `a`, if `α` satisfies the InfConvergenceClass (i.e., is ordered and has a topology such that the limit of a decreasing sequence is its infimum), then the function that coerces elements of `α` to their corresponding type converges to the neighborhood of `a` as `x` approaches negative infinity. In other words, as `x` gets indefinitely small, the values of the function get arbitrarily close to `a`. This is a generalization of the fact that, in the real numbers, a decreasing sequence bounded below converges to its infimum.
More concisely: For any type `α` with a preorder and topology, if it has the InfConvergenceClass property and `s` is a subset of `α` with a greatest lower bound `a`, then the function from `α` to its corresponding type converges to the neighborhood of `a` as `x` approaches negative infinity, for all `x` in `s`.
|
SupConvergenceClass.tendsto_coe_atTop_isLUB
theorem SupConvergenceClass.tendsto_coe_atTop_isLUB :
∀ {α : Type u_3} [inst : Preorder α] [inst_1 : TopologicalSpace α] [self : SupConvergenceClass α] (a : α)
(s : Set α), IsLUB s a → Filter.Tendsto CoeTC.coe Filter.atTop (nhds a)
This theorem states that, for any preordered topological space `α` and a set `s` in `α` where `a` is the least upper bound of `s`, a monotone function will converge to the neighborhood of `a` as `x` approaches infinity. In other words, if a function is sequentially increasing and `a` is the least upper bound of the sequence, then as the function's input grows larger and larger (tends to infinity), the function's output will get arbitrarily close to `a`.
More concisely: If `(α, ≤)` is a preordered topological space, `s ⊆ α` has a least upper bound `a`, and `f : α → ℝ` is a monotone function, then for every neighborhood `V` of `a`, there exists some `x₀ ∈ α` such that for all `x ∈ α` with `x > x₀`, `|f(x) - a| < V`.
|
Monotone.ge_of_tendsto
theorem Monotone.ge_of_tendsto :
∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : Preorder α] [inst_2 : OrderClosedTopology α]
[inst_3 : SemilatticeSup β] {f : β → α} {a : α},
Monotone f → Filter.Tendsto f Filter.atTop (nhds a) → ∀ (b : β), f b ≤ a
This theorem states that for all types `α` and `β` where `α` is equipped with a topological space structure, a preorder (a reflexive and transitive binary relation), and an order closed topology (a topology on a partial order where the closure of any upward-directed set with a least upper bound is that bound), and `β` is equipped with a semilattice structure (a partially ordered set that has a greatest lower bound for any two elements), given a function `f` from `β` to `α` and an element `a` in `α`, if `f` is a monotone function and the limit of `f` as `β` approaches infinity exists and is equal to `a` in the topology on `α`, then for every element `b` in `β`, the function `f` evaluated at `b` is less than or equal to `a`.
In simpler terms, if a function is increasing or non-decreasing and it tends to a certain value as its argument goes to infinity, then all function values are less than or equal to this limit.
More concisely: If `f` is a monotone function from a semilattice `β` to a topological space `α` with an order-closed topology, and the limit of `f(x)` as `x` approaches the greatest element in `β` exists and equals `a` in `α`, then for all `b` in `β`, `f(b) ≤ a`.
|
tendsto_atTop_isLUB
theorem tendsto_atTop_isLUB :
∀ {α : Type u_1} {ι : Type u_3} [inst : Preorder ι] [inst_1 : TopologicalSpace α] [inst_2 : Preorder α]
[inst_3 : SupConvergenceClass α] {f : ι → α} {a : α},
Monotone f → IsLUB (Set.range f) a → Filter.Tendsto f Filter.atTop (nhds a)
The theorem `tendsto_atTop_isLUB` states that for any types `α` and `ι` with `α` having a topology and a preorder, and `α` also being a sup-convergence class, given a function `f` from `ι` to `α` and an element `a` of `α`, if `f` is a monotone function and `a` is a least upper bound of the range of `f`, then `f` tends to `a` at the limit towards infinity. In simpler terms, this theorem ensures that for a non-decreasing function with a least upper bound, the function will converge to this bound as the input approaches infinity.
More concisely: If `α` is a sup-convergence class with a topology and preorder, and `f : ι → α` is a monotone function with `a` as its least upper bound, then `f` converges to `a` as `x` approaches infinity in `ι`.
|