clusterPt_iff_not_disjoint

Mathlib.Topology.ClusterPt

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

English

ClusterPt x F iff not Disjoint (nhds x) F.

Русский

ClusterPt x F тогда и только тогда, когда nhds x и F не несовпадают.

LaTeX

$$$\operatorname{ClusterPt} x F \\iff \\neg \\operatorname{Disjoint}(\\mathcal{N}(x), F)$$$

Lean4

theorem clusterPt_iff_not_disjoint {F : Filter X} : ClusterPt x F ↔ ¬Disjoint (𝓝 x) F := by
  rw [disjoint_iff, ClusterPt, neBot_iff]

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

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

Разделы

Аффилиация

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