completeSpace_iff_ultrafilter — Mathlib

English

A space is complete iff every ultrafilter has a limit point in the space.

Русский

ПолноSpace эквивалентно тому, что каждый ультрафильтр имеет предел внутри пространства.

LaTeX

$$$CompleteSpace(\\alpha) \\iff \\forall l:\\\\ Ultrafilter(\\alpha), Cauchy(l) \\to \\exists x:\\alpha,\\uparrow l \\le 𝓝 x$$$

Lean4

theorem completeSpace_iff_ultrafilter :
    CompleteSpace α ↔ ∀ l : Ultrafilter α, Cauchy (l : Filter α) → ∃ x : α, ↑l ≤ 𝓝 x := by
  simp [completeSpace_iff_isComplete_univ, isComplete_iff_ultrafilter]

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