Ico_filter_le

Mathlib.Order.Interval.Multiset

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

← MathLib Explorer

English

Filtering Ico(a,b) by x ≥ c yields Ico(max(a,c), b).

Русский

Фильтр Ico(a,b) по x ≥ c даёт Ico(max(a,c), b).

LaTeX

$$$ (Ico(a,b)) \cap [c,\infty) = Ico(\max(a,c), b) $$$

Lean4

@[simp]
theorem Ico_filter_le (a b c : α) : ((Ico a b).filter fun x => c ≤ x) = Ico (max a c) b := by
  rw [Ico, Ico, ← Finset.filter_val, Finset.Ico_filter_le]

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

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

Разделы

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

Аффилиация

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