Theorems · Theorem · general topology

tendsto_subseq_of_bounded

• 1000+ list: Bolzano–Weierstrass theorem

∀ {X : Type u_1} [inst : PseudoMetricSpace X] [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)

A version of Bolzano-Weierstrass: in a proper metric space (e.g. $ℝ^n$), every bounded sequence has a converging subsequence.

Defined in

Mathlib.Topology.MetricSpace.Sequences

Cited by

3 results in Mathlib

Foundations

Depth 158 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

PseudoMetricSpaceProperSpace