of_le_nhds'

Mathlib.Topology.ClusterPt

URI: https://scilib.ai/kg/mathlib#ClusterPt.of_le_nhds'

English

If nhds(x) ≤ f for a filter f on X, then x is a cluster point of f.

Русский

Если окрестности x меньше/равны фильтру f, то x является кластерной точкой фильтра f.

LaTeX

$$$\\mathcal{N}(x) \\le f \\Rightarrow \\mathrm{ClusterPt}(x,f)$$$

Lean4

theorem of_le_nhds' {f : Filter X} (H : f ≤ 𝓝 x) (_hf : NeBot f) : ClusterPt x f :=
  ClusterPt.of_le_nhds H

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

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

Разделы

Аффилиация

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