isClosed_setOf_clusterPt — Mathlib

English

The set of cluster points of a filter is closed (in particular, the set of limit points of a sequence).

Русский

Множество кластерных точек фильтра замкнуто (в частности, множество пределов последовательности замкнуто).

LaTeX

$$$IsClosed\{x \mid ClusterPt\ x\ f\}$$$

Lean4

/-- The set of cluster points of a filter is closed. In particular, the set of limit points
of a sequence is closed. -/
theorem isClosed_setOf_clusterPt {f : Filter X} : IsClosed {x | ClusterPt x f} :=
  by
  simp only [clusterPt_iff_forall_mem_closure, setOf_forall]
  exact isClosed_biInter fun _ _ ↦ isClosed_closure

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