range_filter_eq — Mathlib

English

For natural numbers n and m, filtering range n by the condition x = m yields {m} if m < n, otherwise empty.

Русский

Для натуральных чисел n и m фильтрация диапазона n по условию x = m даёт {m}, если m < n, иначе пустое.

LaTeX

$$$(\\mathrm{range}\\ n) \\;\\operatorname{filter} (\\lambda x. x = m) = \\text{if } m < n \\text{ then } \\{m\\} \\text{ else } \\emptyset$$$

Lean4

@[simp]
theorem range_filter_eq {n m : ℕ} : (range n).filter (· = m) = if m < n then { m } else ∅ := by grind

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