mem_closure_iff_ultrafilter — Mathlib

English

A point x belongs to the closure of s if and only if there exists an ultrafilter U with s ∈ U and U ≤ 𝓝 x.

Русский

Точка x принадлежит замыканию множества s тогда и только тогда, когда существует ультрафильтр U с s ∈ U и U ≤ 𝓝 x.

LaTeX

$$$x \\in \\overline{s} \\iff \\exists U : Ultrafilter X, s \\in U \\land U \\le 𝓝 x$$$

Lean4

/-- `x` belongs to the closure of `s` if and only if some ultrafilter
  supported on `s` converges to `x`. -/
theorem mem_closure_iff_ultrafilter : x ∈ closure s ↔ ∃ u : Ultrafilter X, s ∈ u ∧ ↑u ≤ 𝓝 x := by
  simp [closure_eq_cluster_pts, ClusterPt, ← exists_ultrafilter_iff, and_comm]

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