Ico_cons_right

Mathlib.Order.Interval.Multiset

URI: https://scilib.ai/kg/mathlib#Multiset.Ico_cons_right

← MathLib Explorer

English

If b ≤ c, then Ico(a,b) and Ico(c,d) are disjoint.

Русский

Если b ≤ c, то Ico(a,b) и Ico(c,d) взаимно непересекаются.

LaTeX

$$$ b \le c \rightarrow Disjoint (Ico\ a\ b) (Ico\ c\ d) $$$

Lean4

theorem Ico_cons_right (h : a ≤ b) : b ::ₘ Ico a b = Icc a b := by
  classical
  rw [Ico, ← Finset.insert_val_of_notMem right_notMem_Ico, Finset.Ico_insert_right h]
  rfl

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

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

Разделы

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

Аффилиация

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