nhdsLE_eq_nhds

Mathlib.Topology.Order.OrderClosed

URI: https://scilib.ai/kg/mathlib#SuccOrder.nhdsLE_eq_nhds

English

In a succ-order, the left-extends to the real neighborhood: 𝓝[≤] a = 𝓝 a.

Русский

В succ-порядке левая окрестность слывет 𝓝[≤] a = 𝓝 a.

LaTeX

$$$\mathsf{nhds}_{[\le]} a = \mathsf{nhds} a$$$

Lean4

theorem nhdsLE_eq_nhds [SuccOrder α] (a : α) : 𝓝[≤] a = 𝓝 a :=
  PredOrder.nhdsGE_eq_nhds (α := αᵒᵈ) a

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

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

Разделы

Аффилиация

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