English
If m ≤ n then setSeq hf U_mem n ⊆ setSeq hf U_mem m.
Русский
Если m ≤ n, то setSeq hf U_mem n ⊆ setSeq hf U_mem m.
LaTeX
$$$m \le n \Rightarrow \text{setSeq}(hf,U_{mem},n) \subseteq \text{setSeq}(hf,U_{mem},m)$$$
Lean4
/-- A uniform space is complete provided that (a) its uniformity filter has a countable basis;
(b) any sequence satisfying a "controlled" version of the Cauchy condition converges. -/
theorem complete_of_convergent_controlled_sequences (U : ℕ → Set (α × α)) (U_mem : ∀ n, U n ∈ 𝓤 α)
(HU : ∀ u : ℕ → α, (∀ N m n, N ≤ m → N ≤ n → (u m, u n) ∈ U N) → ∃ a, Tendsto u atTop (𝓝 a)) : CompleteSpace α :=
by
obtain ⟨U', -, hU'⟩ := (𝓤 α).exists_antitone_seq
have Hmem : ∀ n, U n ∩ U' n ∈ 𝓤 α := fun n => inter_mem (U_mem n) (hU'.2 ⟨n, Subset.refl _⟩)
refine ⟨fun hf => (HU (seq hf Hmem) fun N m n hm hn => ?_).imp <| le_nhds_of_seq_tendsto_nhds _ _ fun s hs => ?_⟩
· exact inter_subset_left (seq_pair_mem hf Hmem hm hn)
· rcases hU'.1 hs with ⟨N, hN⟩
exact ⟨N, Subset.trans inter_subset_right hN⟩
