filter_lt_of_le_bot — Mathlib

English

If l ≤ n, filtering Ico n m by elements less than l yields the empty list.

Русский

Если l ≤ n, фильтрация Ico n m по элементам меньше l даёт пустой список.

LaTeX

$$$((\operatorname{Ico}(n,m)).\operatorname{filter}(\lambda x. x < l)) = []$$$

Lean4

theorem filter_lt_of_le_bot {n m l : ℕ} (hln : l ≤ n) : ((Ico n m).filter fun x => x < l) = [] :=
  filter_eq_nil_iff.2 fun k hk => by
    simp only [decide_eq_true_eq, not_lt]
    apply le_trans hln
    exact (mem.1 hk).1

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