filter_smul — Mathlib

English

Filtering commutes with scalar multiplication: (r • f).filter p = r • f.filter p.

Русский

Фильтрация коммутирует с умножением на скаляр: (r • f).filter p = r • f.filter p.

LaTeX

$$$$ (r \\cdot f).\\\\mathrm{filter} \\\\mathrm{p} = r \\\\mathrm{of}\\mathrm{filter} \\\\mathrm{p} f $$$$

Lean4

@[simp]
theorem filter_smul [∀ i, Zero (β i)] [∀ i, SMulZeroClass γ (β i)] (p : ι → Prop) [DecidablePred p] (r : γ)
    (f : Π₀ i, β i) : (r • f).filter p = r • f.filter p :=
  by
  ext
  simp [smul_apply, smul_ite]

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