Ico_mem_nhdsLT

Mathlib.Topology.Order.OrderClosed

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

English

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

Русский

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

LaTeX

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

Lean4

theorem Ico_mem_nhdsLT (H : a < b) : Ico a b ∈ 𝓝[<] b :=
  Ico_mem_nhdsLT_of_mem ⟨H, le_rfl⟩

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

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

Разделы

Аффилиация

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