nhdsLE_sup_nhdsGE

Mathlib.Topology.Order.LeftRight

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

English

For a, the supremum of nhdsWithin a [Iic a] and nhdsWithin a [Ici a] equals nhds a.

Русский

Для A наибольшее из nhdsWithin a Iic a и nhdsWithin a Ici a равно nhds a.

LaTeX

$$theorem nhdsLE_sup_nhdsGE (a : α) : 𝓝[≤] a ⊔ 𝓝[≥] a = 𝓝 a$$

Lean4

theorem nhdsLE_sup_nhdsGE (a : α) : 𝓝[≤] a ⊔ 𝓝[≥] a = 𝓝 a := by rw [← nhdsWithin_union, Iic_union_Ici, nhdsWithin_univ]

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

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

Разделы

Аффилиация

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