Ico_mem_nhds

Mathlib.Topology.Order.OrderClosed

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

English

If a < x < b, then Ico(a,b) ∈ 𝓝(x).

Русский

Если a < x < b, то Ico(a,b) принадлежит 𝓝(x).

LaTeX

$$$ a < x \\land x < b \\Rightarrow Ico(a,b) \\in \\mathcal{N}(x) $$$

Lean4

theorem Ico_mem_nhds {a b x : α} (ha : a < x) (hb : x < b) : Ico a b ∈ 𝓝 x :=
  mem_of_superset (Ioo_mem_nhds ha hb) Ioo_subset_Ico_self

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

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

Разделы

Аффилиация

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