prod_filter_mul_prod_filter_not — Mathlib

English

The product of f over g equals the product of its p-filter and its not-p-filter multiplied together.

Русский

Произведение f по g равно произведению по p-фильтру и по фильтру по не-p, перемноженным.

LaTeX

$$$$ (f.filter p).\\mathrm{prod} g \\cdot (f.filter (\\lambda a. \\neg p a)).\\mathrm{prod} g = f\\.prod g. $$$$

Lean4

@[to_additive (attr := simp)]
theorem prod_filter_mul_prod_filter_not [CommMonoid N] (g : α → M → N) :
    (f.filter p).prod g * (f.filter fun a => ¬p a).prod g = f.prod g := by
  simp_rw [prod_filter_index, support_filter, Finset.prod_filter_mul_prod_filter_not, Finsupp.prod]

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