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]