isComplete_iff_ultrafilter' — Mathlib

English

A subset s is complete iff for every ultrafilter l on α, if l is Cauchy and carries s (l ∈ s), then there exists x ∈ s with l converging to x.

Русский

Подмножество S полно тогда и только тогда, когда для каждого ультрафильтра l на α, если l является Cauchy и содержит S, то существует x ∈ S, для которого l сходится к x.

LaTeX

$$$IsComplete(S) \\iff \\forall l:\\\\ Ultrafilter\\ α,\\ Cauchy(l)\\to (s\\in l\\to \\exists x\\in S, l\\le 𝓝 x)$$$

Lean4

theorem isComplete_iff_ultrafilter' {s : Set α} :
    IsComplete s ↔ ∀ l : Ultrafilter α, Cauchy (l : Filter α) → s ∈ l → ∃ x ∈ s, ↑l ≤ 𝓝 x :=
  isComplete_iff_ultrafilter.trans <| by simp only [le_principal_iff, Ultrafilter.mem_coe]

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