filter_lt_of_ge — Mathlib

English

If l ≤ m, then filtering Ico n m by elements less than l yields Ico n l.

Русский

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

LaTeX

$$$\forall n,m,l\ (hlm : l \le m),\ ((\operatorname{Ico}(n,m)).\operatorname{filter}(\lambda x. x < l)) = \operatorname{Ico}(n,l)$$$

Lean4

theorem filter_lt_of_ge {n m l : ℕ} (hlm : l ≤ m) : ((Ico n m).filter fun x => x < l) = Ico n l :=
  by
  rcases le_total n l with hnl | hln
  ·
    rw [← append_consecutive hnl hlm, filter_append, filter_lt_of_top_le (le_refl l), filter_lt_of_le_bot (le_refl l),
      append_nil]
  · rw [eq_nil_of_le hln, filter_lt_of_le_bot hln]

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