Ico_sub_Ico_left

Mathlib.Order.Interval.Multiset

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

← MathLib Explorer

English

Subtracting Ico(a,c) from Ico(a,b) yields Ico(max(a,c), b).

Русский

Из Ico(a,b) вычитаем Ico(a,c) и получаем Ico(max(a,c), b).

LaTeX

$$$ Ico(a,b) - Ico(a,c) = Ico(\max(a,c), b) $$$

Lean4

@[simp]
theorem Ico_sub_Ico_left (a b c : α) : Ico a b - Ico a c = Ico (max a c) b := by
  rw [Ico, Ico, Ico, ← Finset.sdiff_val, Finset.Ico_diff_Ico_left]

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

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

Разделы

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

Аффилиация

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