nhdsGE_eq_nhds

Mathlib.Topology.Order.OrderClosed

URI: https://scilib.ai/kg/mathlib#PredOrder.nhdsGE_eq_nhds

English

In a PredOrder, the ≥-neighborhood equals the standard neighborhood: 𝓝[≥] a = 𝓝 a.

Русский

В предпорядке окрестность слева и вправо согласованы: 𝓝[≥] a = 𝓝 a.

LaTeX

$$$[PredOrder\ α] \; \forall a:\, α,\; 𝓝_{[\ge]}(a) = 𝓝(a)$$$

Lean4

theorem nhdsGE_eq_nhds [PredOrder α] (a : α) : 𝓝[≥] a = 𝓝 a := by rw [← nhdsLT_sup_nhdsGE, PredOrder.nhdsLT, bot_sup_eq]

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

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

Разделы

Аффилиация

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