filter_lt_of_top_le — Mathlib

English

If l ≤ m, filtering Ico n m by elements less than l leaves Ico n m unchanged.

Русский

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

LaTeX

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

Lean4

theorem filter_lt_of_top_le {n m l : ℕ} (hml : m ≤ l) : ((Ico n m).filter fun x => x < l) = Ico n m :=
  filter_eq_self.2 fun k hk => by simp only [(lt_of_lt_of_le (mem.1 hk).2 hml), decide_true]

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