filter_le_of_bot

Mathlib.Data.List.Intervals

URI: https://scilib.ai/kg/mathlib#List.Ico.filter_le_of_bot

← MathLib Explorer

English

For n < m, filtering Ico(n, m) by x ≤ n yields [n].

Русский

Для n < m отсечение Ico(n, m) по x ≤ n даёт [n].

LaTeX

$$$$ n < m \\implies \\{x \\in \\mathbb{N} \\mid n \\le x < m \\land x \\le n\\} = \\{n\\}. $$$$

Lean4

@[simp]
theorem filter_le_of_bot {n m : ℕ} (hnm : n < m) : ((Ico n m).filter fun x => x ≤ n) = [n] :=
  by
  rw [← filter_lt_of_succ_bot hnm]
  exact filter_congr fun _ _ => by simpa using Nat.lt_succ_iff.symm

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

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

Разделы

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

Аффилиация

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