Ioc_mem_nhdsGT

Mathlib.Topology.Order.OrderClosed

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

English

If b ∈ Ico(a, c), then Ico(a, c) lies in the nhdsWithin of b with respect to Ioi b.

Русский

Если b ∈ Ico(a, c), то Ico(a, c) лежит в nhdsWithin б относительно Ioi b.

LaTeX

$$$b \in Ico(a, c) \rightarrow Ico(a, c) \in 𝓝[b] (Ioi b)$$$

Lean4

theorem Ioc_mem_nhdsGT (H : a < b) : Ioc a b ∈ 𝓝[>] a :=
  Ioc_mem_nhdsGT_of_mem ⟨le_rfl, H⟩

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

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

Разделы

Аффилиация

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