English
A subset s of a uniform space α is complete iff for every ultrafilter l on α, if l is Cauchy and respects s (i.e. l ≤ 𝓟 s), then there exists x ∈ s with l converging to x in the neighborhood sense.
Русский
Подмножество S пространства с единицами равномерности α полно, если для каждого ультрафильтра l на α, который является Cauchy и удовлетворяет l ≤ 𝓟 S, существует x ∈ S such that l ≤ 𝓝 x.
LaTeX
$$$IsComplete(S) \\iff \\forall l:\\\\ Ultrafilter\\ α,\\ Cauchy(l)\\to (l \\le 𝓟(S) \\to \\exists x\\in S, l \\le 𝓝 x)$$$
Lean4
theorem isComplete_iff_ultrafilter {s : Set α} :
IsComplete s ↔ ∀ l : Ultrafilter α, Cauchy (l : Filter α) → ↑l ≤ 𝓟 s → ∃ x ∈ s, ↑l ≤ 𝓝 x :=
by
refine ⟨fun h l => h l, fun H => isComplete_iff_clusterPt.2 fun l hl hls => ?_⟩
haveI := hl.1
rcases H (Ultrafilter.of l) hl.ultrafilter_of ((Ultrafilter.of_le l).trans hls) with ⟨x, hxs, hxl⟩
exact ⟨x, hxs, (ClusterPt.of_le_nhds hxl).mono (Ultrafilter.of_le l)⟩
