English
Let f be a filter on α. Then f is Cauchy if and only if NeBot(f) and for every entourage s of α, there exists t ∈ f with t × t ⊆ s.
Русский
Пусть f — фильтр на α. Тогда f является Коши тогда и только тогда, когда f не покоита и для каждого entourages s на α существует t ∈ f с t × t ⊆ s.
LaTeX
$$$ \forall f:\text{Filter }\alpha,\; \text{Cauchy}(f) \iff \text{NeBot}(f) \land \forall s \in 𝓤\_\alpha,\; \exists t \in f,\; t \timesˢ t \subseteq s$$$
Lean4
theorem cauchy_iff {f : Filter α} : Cauchy f ↔ NeBot f ∧ ∀ s ∈ 𝓤 α, ∃ t ∈ f, t ×ˢ t ⊆ s :=
cauchy_iff'.trans <| by simp only [subset_def, Prod.forall, mem_prod_eq, and_imp, forall_mem_comm]
