inf_nhds_atTop

Mathlib.Topology.Order.OrderClosed

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

English

The infimum of the neighborhood of a and the ray atTop is the bottom element.

Русский

Наименьшее верхнее ограничение окрестности точки a и луча atTop равно нулю/нижнему элементу.

LaTeX

$$$ 𝓝 a \sqcap atTop = ⊥ $$$

Lean4

@[simp]
theorem inf_nhds_atTop (a : α) : 𝓝 a ⊓ atTop = ⊥ :=
  (disjoint_nhds_atTop a).eq_bot

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

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

Разделы

Аффилиация

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