filter_le_of_le_bot — Mathlib

English

Let n, m, l be natural numbers with l ≤ n. Then filtering Ico(n, m) by x ≥ l leaves the interval unchanged: ((Ico n m).filter (λ x, l ≤ x)) = Ico n m.

Русский

Пусть n, m, l — натуральные числа и l ≤ n. Тогда отсев Ico(n, m) по условию x ≥ l не изменяет интервал: ((Ico n m).filter (λ x, l ≤ x)) = Ico n m.

LaTeX

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

Lean4

theorem filter_le_of_le_bot {n m l : ℕ} (hln : l ≤ n) : ((Ico n m).filter fun x => l ≤ x) = Ico n m :=
  filter_eq_self.2 fun k hk => by
    rw [decide_eq_true_eq]
    exact le_trans hln (mem.1 hk).1

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