English
Let α be a uniform space and s ⊆ α. Then s is complete iff for every Cauchy filter l on α that is contained in the principal filter of s, there exists a point x in s which is a cluster point of l.
Русский
Пусть α — равномерное пространство, и S ⊆ α. Тогда S полно тогда, когда для каждого Cauchy-фильтра l на α, удовлетворяющего l ≤ 𝓟(S), существует точка x ∈ S такая, что x является кластерной точкой l.
LaTeX
$$$\\text{IsComplete}(S) \\iff \\forall l\\, (\\text{Cauchy}(l) \\rightarrow l \\le \\mathcal{P}(S) \\rightarrow \\exists x\\in S, \\ ClusterPt\\ x\\ l)$$$
Lean4
theorem isComplete_iff_clusterPt {s : Set α} : IsComplete s ↔ ∀ l, Cauchy l → l ≤ 𝓟 s → ∃ x ∈ s, ClusterPt x l :=
forall₃_congr fun _ hl _ => exists_congr fun _ => and_congr_right fun _ => le_nhds_iff_adhp_of_cauchy hl
