nhds_neBot

Mathlib.Topology.Neighborhoods

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

English

The neighborhood filter at any x is not the bottom filter; i.e., nhds x ≠ ⊥.

Русский

Фильтр окрестностей в любой точке не равен нижнему фильтру; то есть nhds x не равно ⊥.

LaTeX

$$$\\text{nhds } x \\text{ is not bottom: } (nhds x) \\NeBot.$$$

Lean4

@[simp]
instance nhds_neBot : NeBot (𝓝 x) :=
  neBot_of_le (pure_le_nhds x)

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

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

Разделы

Аффилиация

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