Ico_insert_right

Mathlib.Order.Interval.Finset.Basic

URI: https://scilib.ai/kg/mathlib#Finset.Ico_insert_right

← MathLib Explorer

English

If a ≤ b, then inserting b into Ico a b yields Icc a b.

Русский

Если a ≤ b, то добавление b в Ico a b дает Icc a b.

LaTeX

$$$\text{insert } b (\mathrm{Ico}(a,b)) = \mathrm{Icc}(a,b) \quad (\text{when } a \le b).$$$

Lean4

@[simp]
theorem Ico_insert_right (h : a ≤ b) : insert b (Ico a b) = Icc a b := by
  rw [← coe_inj, coe_insert, coe_Icc, coe_Ico, Set.insert_eq, Set.union_comm, Set.Ico_union_right h]

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

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

Разделы

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

Аффилиация

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