nhdsLT_sup_nhdsGE

Mathlib.Topology.Order.LeftRight

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

English

The supremum of nhdsWithin a (Iio a) and nhdsWithin a (Ici a) equals nhdsWithin a a.

Русский

Наибольшее из nhdsWithin a Iio a и nhdsWithin a Ici a равно nhdsWithin a a.

LaTeX

$$theorem nhdsLT_sup_nhdsWithinGE (a : α) : 𝓝[<] a ⊔ 𝓝[≥] a = 𝓝 a$$

Lean4

theorem nhdsLT_sup_nhdsGE (a : α) : 𝓝[<] a ⊔ 𝓝[≥] a = 𝓝 a := by rw [← nhdsWithin_union, Iio_union_Ici, nhdsWithin_univ]

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

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

Разделы

Аффилиация

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