English
If the uniformity has a basis with p and s, then CauchySeq u is equivalent to a basis criterion in terms of N and indices.
Русский
Если униформность имеет базис с p и s, то КошиSeq эквивалентно базисной мере через N и индексы.
LaTeX
$$$\\text{HasBasis}(p,s) \\Rightarrow \\text{CauchySeq}(u) \\iff \\forall i, p(i) \\Rightarrow \\exists N,\\forall m,n \\ge N, (u(m),u(n)) \\in s(i).$$$
Lean4
theorem cauchySeq_iff {γ} [Nonempty β] [SemilatticeSup β] {u : β → α} {p : γ → Prop} {s : γ → Set (α × α)}
(h : (𝓤 α).HasBasis p s) : CauchySeq u ↔ ∀ i, p i → ∃ N, ∀ m, N ≤ m → ∀ n, N ≤ n → (u m, u n) ∈ s i :=
by
rw [cauchySeq_iff_tendsto, ← prod_atTop_atTop_eq]
refine (atTop_basis.prod_self.tendsto_iff h).trans ?_
simp only [true_and, Prod.forall, mem_prod_eq, mem_Ici, and_imp, Prod.map, @forall_swap (_ ≤ _) β]
