filter_le_of_le — Mathlib

English

For any n, m, l with l ≤ n, filtering Ico(n, m) by x ≥ l yields Ico(l, m).

Русский

Для любых n, m, l с l ≤ n отсечение Ico(n, m) по x ≥ l даёт Ico(l, m).

LaTeX

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

Lean4

theorem filter_le_of_le {n m l : ℕ} (hnl : n ≤ l) : ((Ico n m).filter fun x => l ≤ x) = Ico l m :=
  by
  rcases le_total l m with hlm | hml
  ·
    rw [← append_consecutive hnl hlm, filter_append, filter_le_of_top_le (le_refl l), filter_le_of_le_bot (le_refl l),
      nil_append]
  · rw [eq_nil_of_le hml, filter_le_of_top_le hml]

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