isClosed_iff_ultrafilter — Mathlib

English

A set s is closed if and only if for every x and every ultrafilter u with u ≤ 𝓝 x, if s ∈ u then x ∈ s.

Русский

Множество s замкнуто тогда, когда для каждого x и каждого ультрафильтра u с u ≤ 𝓝 x, если s ∈ u, тогда x ∈ s.

LaTeX

$$$IsClosed(s) \\iff \\forall x, \\forall u : Ultrafilter X, u \\le 𝓝 x \\rightarrow s \\in u \\rightarrow x \\in s$$$

Lean4

theorem isClosed_iff_ultrafilter : IsClosed s ↔ ∀ x, ∀ u : Ultrafilter X, ↑u ≤ 𝓝 x → s ∈ u → x ∈ s := by
  simp [isClosed_iff_clusterPt, ClusterPt, ← exists_ultrafilter_iff]

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