English
A sequentially compact set in a uniform space is totally bounded.
Русский
Последовательнос-но компактное множество в равномерном пространстве является тотально ограниченным.
LaTeX
$$$IsSeqCompact s \Rightarrow TotallyBounded s$$$
Lean4
/-- A sequentially compact set in a uniform space is totally bounded. -/
protected theorem totallyBounded (h : IsSeqCompact s) : TotallyBounded s :=
by
intro V V_in
unfold IsSeqCompact at h
contrapose! h
obtain ⟨u, u_in, hu⟩ : ∃ u : ℕ → X, (∀ n, u n ∈ s) ∧ ∀ n m, m < n → u m ∉ ball (u n) V :=
by
simp only [not_subset, mem_iUnion₂, not_exists, exists_prop] at h
simpa only [forall_and, forall_mem_image, not_and] using seq_of_forall_finite_exists h
refine ⟨u, u_in, fun x _ φ hφ huφ => ?_⟩
obtain ⟨N, hN⟩ : ∃ N, ∀ p q, p ≥ N → q ≥ N → (u (φ p), u (φ q)) ∈ V := huφ.cauchySeq.mem_entourage V_in
exact hu (φ <| N + 1) (φ N) (hφ <| Nat.lt_add_one N) (hN (N + 1) N N.le_succ le_rfl)
