English
For any f on α, f is Cauchy if and only if f is nonempty and for every entourage s of α there exists a set t ∈ f with the property that all pairs of points from t are within s.
Русский
Для любого фильтра f на α фильтр Коши тогда и только тогда, когда он непуст и для каждого entourages s в α существует множество t ∈ f такое, что любые две точки x,y ∈ t удовлетворяют (x,y) ∈ s.
LaTeX
$$$ \forall f:\text{Filter }\alpha,\; \text{Cauchy}(f) \iff \text{NeBot}(f) \land \forall s \in 𝓤\_\alpha,\; \exists t \in f,\; \forall x \in t,\; \forall y \in t,\; (x,y) \in s$$$
Lean4
theorem cauchy_iff' {f : Filter α} : Cauchy f ↔ NeBot f ∧ ∀ s ∈ 𝓤 α, ∃ t ∈ f, ∀ x ∈ t, ∀ y ∈ t, (x, y) ∈ s :=
(𝓤 α).basis_sets.cauchy_iff
