nhdsLE_neBot

Mathlib.Topology.Order.LeftRight

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

English

For any a, the neighborhood within the lower ray [≤] a is nonempty.

Русский

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

LaTeX

$$$(a : \\alpha) \\Rightarrow (\\mathcal{N}_{[\\le] a}).NeBot$$$

Lean4

instance nhdsLE_neBot (a : α) : NeBot (𝓝[≤] a) :=
  nhdsWithin_Iic_neBot (le_refl a)

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

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

Разделы

Аффилиация

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