nhdsGE_neBot

Mathlib.Topology.Order.LeftRight

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

English

For any a, the neighborhood filter within the ray [≥] a is nonempty.

Русский

Для любого a фильтр окрестностей внутри луча [≥] a непуст.

LaTeX

$$∀ a, (𝓝[≥] a).NeBot$$

Lean4

instance nhdsGE_neBot (a : α) : NeBot (𝓝[≥] a) :=
  nhdsWithin_Ici_neBot (le_refl a)

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

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

Разделы

Аффилиация

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