filter_lt — Mathlib

English

Let n, m, l be natural numbers. Then the list Ico(n, m) filtered by x < l equals Ico(n, min(m, l)).

Русский

Пусть n, m, l натуральные числа. Тогда список Ico(n, m), отфильтрованный по условию x < l, равен Ico(n, min(m, l)).

LaTeX

$$$$ Ico(n,m) \\cap \\{x \\in \\mathbb{N} \\mid x < l\\} = Ico\\bigl(n, \\min(m,l)\\bigr). $$$$

Lean4

@[simp]
theorem filter_lt (n m l : ℕ) : ((Ico n m).filter fun x => x < l) = Ico n (min m l) :=
  by
  rcases le_total m l with hml | hlm
  · rw [min_eq_left hml, filter_lt_of_top_le hml]
  · rw [min_eq_right hlm, filter_lt_of_ge hlm]

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