Ico_insert_succ_left

Mathlib.Order.Interval.Finset.Nat

URI: https://scilib.ai/kg/mathlib#Nat.Ico_insert_succ_left

← MathLib Explorer

English

If a < b, then inserting a into Ico(a+1, b) yields Ico(a, b).

Русский

Если a < b, то вставка a в Ico(a+1, b) дает Ico(a, b).

LaTeX

$$$(\\mathrm{insert}\ a (Ico(a+1,b))) = Ico(a,b)$$$

Lean4

@[deprecated Finset.insert_Ico_succ_left_eq_Ico (since := "2025-04-24")]
theorem Ico_insert_succ_left (h : a < b) : insert a (Ico a.succ b) = Ico a b := by
  rw [Ico_succ_left, ← Ioo_insert_left h]

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

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

Разделы

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

Аффилиация

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