English
A filter f on a uniform space is Cauchy if it is nontrivial and f ×ˢ f ≤ 𝓤 α.
Русский
Фильтр f на равномерном пространстве называется Cauchy, если он неравен и выполняется f ×ˢ f ≤ 𝓤 α.
LaTeX
$$Cauchy f := NeBot f ∧ f ×ˢ f ≤ 𝓤 α$$
Lean4
/-- A filter `f` is Cauchy if for every entourage `r`, there exists an
`s ∈ f` such that `s × s ⊆ r`. This is a generalization of Cauchy
sequences, because if `a : ℕ → α` then the filter of sets containing
cofinitely many of the `a n` is Cauchy iff `a` is a Cauchy sequence. -/
def Cauchy (f : Filter α) :=
NeBot f ∧ f ×ˢ f ≤ 𝓤 α