English
Let (β_i) be a family of Abelian groups indexed by ι, and f be a finitely supported family with values in these groups. Then negation commutes with filtering by any predicate p: ι → Prop, i.e. (-f).filter p = -(f.filter p).
Русский
Пусть (β_i) — семейство абелевых групп, индексируемое по ι, а f — конечно-поддерживаемая функция с значениями в этих группах. Тогда отрицание применяется по каждому индексу до фильтрации, и фильтр сохраняет свойство; т.е. (-f).filter p = -(f.filter p).
LaTeX
$$$(-f).filter p = -(f.filter p)$$$
Lean4
@[simp]
theorem filter_neg [∀ i, AddGroup (β i)] (p : ι → Prop) [DecidablePred p] (f : Π₀ i, β i) :
(-f).filter p = -f.filter p :=
(filterAddMonoidHom β p).map_neg f
