nhdsLE_sup_nhdsGT

Mathlib.Topology.Order.LeftRight

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

English

The supremum of nhdsWithin a (Iic a) and nhdsWithin a (Ioi a) equals nhds a.

Русский

Наибольшее из nhdsWithin a Iic a и nhdsWithin a Ioi a равно nhds a.

LaTeX

$$theorem nhdsLE_sup_nhdsGT (a : α) : 𝓝[≤] a ⊔ 𝓝[>] a = 𝓝 a$$

Lean4

theorem nhdsLE_sup_nhdsGT (a : α) : 𝓝[≤] a ⊔ 𝓝[>] a = 𝓝 a := by rw [← nhdsWithin_union, Iic_union_Ioi, nhdsWithin_univ]

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

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

Разделы

Аффилиация

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