English
Let A be a uniform space and s ⊆ A. The subset s is complete if every Cauchy filter f that contains s has a limit in s; equivalently, for every Cauchy filter f with s ∈ f, there exists x ∈ s such that f ≤ nhds x.
Русский
Пусть A — равномерное пространство и s ⊆ A. Подмножество s называется полным, если каждый Коши-фильтр f, удовлетворяющий условию s ∈ f, имеет предел в s; эквивалентно: для каждого Коши-фильтра f с s ∈ f существует x ∈ s такой, что f ≤ nhds x.
LaTeX
$$$ \forall f\, (\text{Cauchy}(f) \rightarrow f \le 𝓟 s \rightarrow ∃ x \in s,\ f \le 𝓝 x)$$$
Lean4
/-- A set `s` is called *complete*, if any Cauchy filter `f` such that `s ∈ f`
has a limit in `s` (formally, it satisfies `f ≤ 𝓝 x` for some `x ∈ s`). -/
def IsComplete (s : Set α) :=
∀ f, Cauchy f → f ≤ 𝓟 s → ∃ x ∈ s, f ≤ 𝓝 x
