Ico_sub_Ico_right

Mathlib.Order.Interval.Multiset

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

← MathLib Explorer

English

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

Русский

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

LaTeX

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

Lean4

@[simp]
theorem Ico_sub_Ico_right (a b c : α) : Ico a b - Ico c b = Ico a (min b c) := by
  rw [Ico, Ico, Ico, ← Finset.sdiff_val, Finset.Ico_diff_Ico_right]

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

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

Разделы

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

Аффилиация

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