nhdsWithinLE_sup_nhdsWithinGE

Mathlib.Topology.Order.LeftRight

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

← MathLib Explorer

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 nhdsWithinLE_sup_nhdsWithinGE (a : α) : 𝓝[s ∩ Iic a] a ⊔ 𝓝[s ∩ Ici a] a = 𝓝[s] a := by
  rw [← nhdsWithin_union, ← inter_union_distrib_left, Iic_union_Ici, inter_univ]

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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