clusterPt

Mathlib.Topology.ClusterPt

URI: https://scilib.ai/kg/mathlib#AccPt.clusterPt

English

Every accumulation point is a cluster point.

Русский

Каждая накопленная точка является кластерной точкой.

LaTeX

$$$AccPt\ x\ F \Rightarrow ClusterPt\ x\ F$$$

Lean4

theorem clusterPt {x : X} {F : Filter X} (h : AccPt x F) : ClusterPt x F :=
  (accPt_iff_clusterPt.mp h).mono inf_le_right

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

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

Разделы

Аффилиация

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