filter_le_of_top_le — Mathlib

English

Let n, m, l be natural numbers with m ≤ l. Then filtering Ico(n, m) by x ≥ l yields the empty list.

Русский

Пусть n, m, l — натуральные числа и m ≤ l. Тогда отсев Ico(n, m) по x ≥ l даёт пустой список.

LaTeX

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

Lean4

theorem filter_le_of_top_le {n m l : ℕ} (hml : m ≤ l) : ((Ico n m).filter fun x => l ≤ x) = [] :=
  filter_eq_nil_iff.2 fun k hk => by
    rw [decide_eq_true_eq]
    exact not_le_of_gt (lt_of_lt_of_le (mem.1 hk).2 hml)

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