pure_le_nhds

Mathlib.Topology.Neighborhoods

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

English

The principal filter at x is less than or equal to the neighborhood filter at x: pure x ≤ nhds x.

Русский

Принципиальный фильтр в точке x не превосходит фильтр окрестностей в x.

LaTeX

$$$\\text{pure} \\le (\\mathcal{N} : X \\to \\text{Filter } X).$$$

Lean4

theorem pure_le_nhds : pure ≤ (𝓝 : X → Filter X) := fun _ _ hs => mem_pure.2 <| mem_of_mem_nhds hs

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

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

Разделы

Аффилиация

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