Cauchy — Mathlib

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 ≤ 𝓤 α

Похожие утверждения