English
For any predicate p, multiset s, and n ∈ ℕ, filtering after n-fold summation equals n-fold filtering: filter p (n • s) = n • filter p s.
Русский
Для предиката p, мультимножества s и n ∈ ℕ выполняется фильтрация после n-раз суммирования равна n-кратно фильтрованию: filter p (n • s) = n • filter p s.
LaTeX
$$$\text{filter}_p (n \cdot s) = n \cdot \text{filter}_p(s).$$$
Lean4
theorem filter_nsmul (s : Multiset α) (n : ℕ) : filter p (n • s) = n • filter p s :=
by
refine s.induction_on ?_ ?_
· simp only [filter_zero, nsmul_zero]
· intro a ha ih
rw [nsmul_cons, filter_add, ih, filter_cons, nsmul_add]
congr
split_ifs with hp <;>
· simp only [filter_eq_self, nsmul_zero, filter_eq_nil]
intro b hb
rwa [mem_singleton.mp (mem_of_mem_nsmul hb)]
