Ico_succ_left_eq_erase_Ico

Mathlib.Order.Interval.Finset.Nat

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

← MathLib Explorer

English

For any a,b, Ico(a+1,b) equals erase(Ico(a,b), a).

Русский

Для любых a,b, Ico(a+1,b) = erase(Ico(a,b), a).

LaTeX

$$$Ico(a.succ, b) = \\mathrm{erase} (Ico(a,b)) a$$$

Lean4

theorem Ico_succ_left_eq_erase_Ico : Ico a.succ b = erase (Ico a b) a :=
  by
  ext x
  rw [Ico_succ_left, mem_erase, mem_Ico, mem_Ioo, ← and_assoc, ne_comm, and_comm (a := a ≠ x), lt_iff_le_and_ne]

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

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

Разделы

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

Аффилиация

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