English
Filtering after scaling equals scaling after filtering: for any predicate p, (b • v).filter p = b • (v.filter p) when M has SMulZero and zero is preserved.
Русский
Фильтрация после масштабирования равна масштабированию после фильтрации: для любого p выполняется (b • v).filter p = b • (v.filter p).
LaTeX
$$$[DecidablePred p][Zero M][SMulZeroClass R M] \\, {b : R} \\; {v : \\alpha \\to_0 M} \\, \\Rightarrow \\, (b \\cdot v).\\mathrm{filter} \\, p = b \\cdot (v.\\mathrm{filter} \\, p)$$$
Lean4
@[simp]
theorem filter_smul [Zero M] [SMulZeroClass R M] {b : R} {v : α →₀ M} : (b • v).filter p = b • v.filter p :=
DFunLike.coe_injective <| by
simp only [filter_eq_indicator, coe_smul]
exact Set.indicator_const_smul {x | p x} b v
