Ico_filter_lt_of_le_left — Mathlib

English

If c ≤ a, then filtering Ico(a,b) by x < c yields the empty multiset.

Русский

Если c ≤ a, то фильтрация Ico(a,b) по x < c даёт пустое множество/множество.

LaTeX

$$$ c \le a \rightarrow ((Ico\ a\ b).filter\ (\lambda x. x < c)) = 0 $$$

Lean4

theorem Ico_filter_lt_of_le_left [DecidablePred (· < c)] (hca : c ≤ a) : ((Ico a b).filter fun x => x < c) = ∅ :=
  by
  rw [Ico, ← Finset.filter_val, Finset.Ico_filter_lt_of_le_left hca]
  rfl

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