Documentation

Mathlib.Topology.MetricSpace.Sequences

Sequential compacts in metric spaces #

In this file we prove 2 versions of Bolzano-Weierstrass theorem for proper metric spaces.

@[deprecated SeqCompact.lebesgue_number_lemma_of_metric]
theorem SeqCompact.lebesgue_number_lemma_of_metric {X : Type u_1} [PseudoMetricSpace X] {ι : Sort u_2} {c : ιSet X} {s : Set X} (hs : IsSeqCompact s) (hc₁ : ∀ (i : ι), IsOpen (c i)) (hc₂ : s ⋃ (i : ι), c i) :
δ > 0, as, ∃ (i : ι), Metric.ball a δ c i
theorem tendsto_subseq_of_frequently_bounded {X : Type u_1} [PseudoMetricSpace X] [ProperSpace X] {s : Set X} (hs : Bornology.IsBounded s) {x : X} (hx : ∃ᶠ (n : ) in Filter.atTop, x n s) :
aclosure s, ∃ (φ : ), StrictMono φ Filter.Tendsto (x φ) Filter.atTop (nhds a)

A version of Bolzano-Weierstrass: in a proper metric space (eg. $ℝ^n$), every bounded sequence has a converging subsequence. This version assumes only that the sequence is frequently in some bounded set.

theorem tendsto_subseq_of_bounded {X : Type u_1} [PseudoMetricSpace X] [ProperSpace X] {s : Set X} (hs : Bornology.IsBounded s) {x : X} (hx : ∀ (n : ), x n s) :
aclosure s, ∃ (φ : ), StrictMono φ Filter.Tendsto (x φ) Filter.atTop (nhds a)

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