English
A sequentially compact set in a uniform space with countably generated uniformity is complete.
Русский
Последовательнос-но компактное множество в равномерном пространстве с счетной порожденностью тождественно полно.
LaTeX
$$$IsSeqCompact s \Rightarrow IsComplete s$ (in a uniform space with countably generated uniformity).$$
Lean4
/-- A sequentially compact set in a uniform space with countably generated uniformity filter
is complete. -/
protected theorem isComplete (hs : IsSeqCompact s) : IsComplete s := fun l hl hls =>
by
have := hl.1
rcases exists_antitone_basis (𝓤 X) with ⟨V, hV⟩
choose W hW hWV using fun n => comp_mem_uniformity_sets (hV.mem n)
have hWV' : ∀ n, W n ⊆ V n := fun n ⟨x, y⟩ hx => @hWV n (x, y) ⟨x, refl_mem_uniformity <| hW _, hx⟩
obtain ⟨t, ht_anti, htl, htW, hts⟩ :
∃ t : ℕ → Set X, Antitone t ∧ (∀ n, t n ∈ l) ∧ (∀ n, t n ×ˢ t n ⊆ W n) ∧ ∀ n, t n ⊆ s :=
by
have : ∀ n, ∃ t ∈ l, t ×ˢ t ⊆ W n ∧ t ⊆ s :=
by
rw [le_principal_iff] at hls
have : ∀ n, W n ∩ s ×ˢ s ∈ l ×ˢ l := fun n => inter_mem (hl.2 (hW n)) (prod_mem_prod hls hls)
simpa only [l.basis_sets.prod_self.mem_iff, true_imp_iff, subset_inter_iff, prod_self_subset_prod_self,
and_assoc] using this
choose t htl htW hts using this
have : ∀ n : ℕ, ⋂ k ≤ n, t k ⊆ t n := fun n => by apply iInter₂_subset; rfl
exact
⟨fun n => ⋂ k ≤ n, t k, fun m n h => biInter_subset_biInter_left fun k (hk : k ≤ m) => hk.trans h, fun n =>
(biInter_mem (finite_le_nat n)).2 fun k _ => htl k, fun n => (prod_mono (this n) (this n)).trans (htW n),
fun n => (this n).trans (hts n)⟩
choose u hu using fun n => Filter.nonempty_of_mem (htl n)
have huc : CauchySeq u :=
hV.toHasBasis.cauchySeq_iff.2 fun N _ =>
⟨N, fun m hm n hn => hWV' _ <| @htW N (_, _) ⟨ht_anti hm (hu _), ht_anti hn (hu _)⟩⟩
rcases hs.exists_tendsto (fun n => hts n (hu n)) huc with ⟨x, hxs, hx⟩
refine ⟨x, hxs, (nhds_basis_uniformity' hV.toHasBasis).ge_iff.2 fun N _ => ?_⟩
obtain ⟨n, hNn, hn⟩ : ∃ n, N ≤ n ∧ u n ∈ ball x (W N) :=
((eventually_ge_atTop N).and (hx <| ball_mem_nhds x (hW N))).exists
refine mem_of_superset (htl n) fun y hy => hWV N ⟨u n, hn, htW N ?_⟩
exact ⟨ht_anti hNn (hu n), ht_anti hNn hy⟩
