Ioc_mem_nhdsLT

Mathlib.Topology.Order.OrderClosed

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

English

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

Русский

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

LaTeX

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

Lean4

theorem Ioc_mem_nhdsLT (H : a < b) : Ioc a b ∈ 𝓝[<] b :=
  Ioc_mem_nhdsLT_of_mem ⟨H, le_rfl⟩

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

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

Разделы

Аффилиация

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