tendsto_subseq_of_frequently_bounded
theorem tendsto_subseq_of_frequently_bounded :
∀ {X : Type u_1} [inst : PseudoMetricSpace X] [inst_1 : ProperSpace X] {s : Set X},
Bornology.IsBounded s →
∀ {x : ℕ → X},
(∃ᶠ (n : ℕ) in Filter.atTop, x n ∈ s) →
∃ a ∈ closure s, ∃ φ, StrictMono φ ∧ Filter.Tendsto (x ∘ φ) Filter.atTop (nhds a)
This is a version of the Bolzano-Weistrass Theorem: In a proper metric space (for example, $\mathbb{R}^n$), every bounded sequence has a converging subsequence. This particular version only assumes that the sequence is frequently in some bounded set. More specifically, given a set `s` that is bounded in the context of a pseudo-metric space that is also a proper space, and a sequence `x` of elements in this space such that the elements of `x` are frequently in `s` (with respect to a filter representing the limit towards infinity), there exists an element `a` in the closure of `s` and a strictly monotonic function `φ` such that the composition of `x` and `φ` tends towards `a` as we go towards infinity.
More concisely: In a proper metric space, every bounded sequence with infinitely many elements in a given bounded set has a convergent subsequence that converges to a limit in the closure of that set.
|
tendsto_subseq_of_bounded
theorem tendsto_subseq_of_bounded :
∀ {X : Type u_1} [inst : PseudoMetricSpace X] [inst_1 : ProperSpace X] {s : Set X},
Bornology.IsBounded s →
∀ {x : ℕ → X},
(∀ (n : ℕ), x n ∈ s) → ∃ a ∈ closure s, ∃ φ, StrictMono φ ∧ Filter.Tendsto (x ∘ φ) Filter.atTop (nhds a)
This is a version of the **Bolzano-Weistrass** theorem, which states that in a proper metric space (such as ℝⁿ), every bounded sequence has a converging subsequence. More specifically, given a set `s` in a pseudo-metric space `X` that is also a proper space, if `s` is bounded, then for any sequence `x` of natural numbers such that every element of `x` is in `s`, there exists an element `a` in the closure of `s` and a strictly monotone function `φ` such that the composition of `x` and `φ` tends to `a` as we approach infinity.
More concisely: In a proper metric space, every bounded sequence has a convergent subsequence whose limit is in the closure of the space.
|