nhdsWithin_Ico_eq_nhdsLT

Mathlib.Topology.Order.OrderClosed

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

English

If b ∈ Ioc a c, then Icc a c is a left-neighborhood of b.

Русский

Если b ∈ Ioc a c, то Icc a c является левой окрестностью b.

LaTeX

$$$(b \in Ioc\ a\ c) \Rightarrow Icc(a,c) \in \mathcal{N}_{[<]}(b)$$$

Lean4

@[simp]
theorem nhdsWithin_Ico_eq_nhdsLT (h : a < b) : 𝓝[Ico a b] b = 𝓝[<] b :=
  nhdsWithin_inter_of_mem <| nhdsWithin_le_nhds <| Ici_mem_nhds h

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

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

Разделы

Аффилиация

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