filter_le — Mathlib

English

For all n, m, l in N, the filter of Ico(n,m) by x ≥ l equals Ico(max(n,l), m).

Русский

Для всех n, m, l в ℕ фильтр Ico(n,m) по x ≥ l равен Ico(max(n,l), m).

LaTeX

$$$$ \\{x \\in \\mathbb{N} \\mid n \\le x < m \\land x \\ge l\\} = \\{x \\in \\mathbb{N} \\mid \\max(n,l) \\le x < m\\}. $$$$

Lean4

@[simp]
theorem filter_le (n m l : ℕ) : ((Ico n m).filter fun x => l ≤ x) = Ico (max n l) m :=
  by
  rcases le_total n l with hnl | hln
  · rw [max_eq_right hnl, filter_le_of_le hnl]
  · rw [max_eq_left hln, filter_le_of_le_bot hln]

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