Ico_filter_lt_of_le_right

Mathlib.Order.Interval.Multiset

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

← MathLib Explorer

English

If c ≤ b, filtering Ico(a,b) by x < c yields Ico(a,c).

Русский

Если c ≤ b, фильтрация Ico(a,b) по x < c даёт Ico(a,c).

LaTeX

$$$ c \le b \rightarrow ((Ico\ a\ b).filter (\lambda x. x < c)) = Ico\ a\ c $$$

Lean4

theorem Ico_filter_lt_of_le_right [DecidablePred (· < c)] (hcb : c ≤ b) : ((Ico a b).filter fun x => x < c) = Ico a c :=
  by
  rw [Ico, ← Finset.filter_val, Finset.Ico_filter_lt_of_le_right hcb]
  rfl

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

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

Разделы

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

Аффилиация

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