closure_eq_cluster_pts

Mathlib.Topology.ClusterPt

URI: https://scilib.ai/kg/mathlib#closure_eq_cluster_pts

English

The closure of a set s is the set of points a such that a is a cluster point of s.

Русский

Замыкание множества s состоит из таких точек a, которые являются кластерными точками s.

LaTeX

$$$\overline{s} = \{a \mid ClusterPt\ a\ (\mathcal{P} s)\}$$$

Lean4

theorem closure_eq_cluster_pts : closure s = {a | ClusterPt a (𝓟 s)} :=
  Set.ext fun _ => mem_closure_iff_clusterPt

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru