Ico_filter_lt

Mathlib.Order.Interval.Multiset

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

← MathLib Explorer

English

Filtering Ico(a,b) by x < c yields Ico(a, min(b,c)).

Русский

Фильтр множества Ico(a,b) по условию x < c даёт Ico(a, min(b,c)).

LaTeX

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

Lean4

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

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

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

Разделы

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

Аффилиация

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