nhdsWithin_Ioo_eq_nhdsLT

Mathlib.Topology.Order.OrderClosed

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

English

For a < b, the left-neighborhood within Ico a b coincides with the left-neighborhood of b: 𝓝[Ico a b] b = 𝓝[<] b.

Русский

Для a < b левое окрестное внутри Ico a b совпадает с левым окрестностью b: 𝓝[Ico a b] b = 𝓝[<] b.

LaTeX

$$$(a

Lean4

@[simp]
theorem nhdsWithin_Ioo_eq_nhdsLT (h : a < b) : 𝓝[Ioo a b] b = 𝓝[<] b :=
  nhdsWithin_inter_of_mem <| nhdsWithin_le_nhds <| Ioi_mem_nhds h

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

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

Разделы

Аффилиация

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