Ioo_subset_uIoo'

Mathlib.Order.Interval.Set.UnorderedInterval

URI: https://scilib.ai/kg/mathlib#Set.Ioo_subset_uIoo'

← MathLib Explorer

English

The open interval Ioo b a is contained in uIoo a b.

Русский

Открытый интервал Ioo b a вложен в uIoo a b.

LaTeX

$$$ Ioo(b,a) \subseteq uIoo(a,b) $$$

Lean4

/-- Same as `Ioo_subset_uIoo` but with `Ioo a b` replaced by `Ioo b a`. -/
theorem Ioo_subset_uIoo' : Ioo b a ⊆ uIoo a b :=
  Ioo_subset_Ioo inf_le_right le_sup_left

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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