inf_nhds_atBot

Mathlib.Topology.Order.OrderClosed

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

English

The infimum of nhds(a) and atBot is the bottom element.

Русский

Наименьшее значения nhds(a) и atBot равно нижнему пределу.

LaTeX

$$nhds(a) ⊓ atBot = ⊥$$

Lean4

@[simp]
theorem inf_nhds_atBot (a : α) : 𝓝 a ⊓ atBot = ⊥ :=
  (disjoint_nhds_atBot a).eq_bot

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

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

Разделы

Аффилиация

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