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, ∀ a ∈ s, ∃ (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) : ∃ a ∈ closure 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) : ∃ a ∈ closure 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.