English
If the uniformity on α has a basis (p, s), then a filter f on α is Cauchy if and only if f is nonempty and, for every index i with p(i), there exists t ∈ f such that t × t ⊆ s(i).
Русский
Если равномерность на α имеет базис (p, s), то фильтр f на α является Коши тогда и только тогда, когда он не пуст, и для каждого индекса i с p(i) существует t ∈ f such that t × t ⊆ s(i).
LaTeX
$$$ (\mathcal{U}\_\alpha).HasBasis p\, s \; \Longrightarrow\; (\text{Cauchy}(f) \iff \text{NeBot}(f) \land \forall i,\ p(i) \to \exists t \in f, \forall x \in t, \forall y \in t, (x,y) \in s(i))$$$
Lean4
theorem cauchy_iff {ι} {p : ι → Prop} {s : ι → Set (α × α)} (h : (𝓤 α).HasBasis p s) {f : Filter α} :
Cauchy f ↔ NeBot f ∧ ∀ i, p i → ∃ t ∈ f, ∀ x ∈ t, ∀ y ∈ t, (x, y) ∈ s i :=
and_congr Iff.rfl <|
(f.basis_sets.prod_self.le_basis_iff h).trans <| by
simp only [subset_def, Prod.forall, mem_prod_eq, and_imp, id, forall_mem_comm]
