prod_filter_mul_prod_filter_not — Mathlib

English

Let p be a predicate with decidable predicate. Then (s.filter p).prod · (s.filter (not p)).prod = s.prod.

Русский

Пусть p — дизъективное свойство; тогда произведение элементов s, удовлетворяющих p, умноженное на произведение остальных элементов, равно произведению всего s.

LaTeX

$$$ \mathrm{prod}(\mathrm{filter}\ p\ s) \cdot \mathrm{prod}(\mathrm{filter}\ (fun x \rightarrow \lnot p x)\ s) = \mathrm{prod}(s) $$$

Lean4

@[to_additive]
theorem prod_filter_mul_prod_filter_not (p) [DecidablePred p] :
    (s.filter p).prod * (s.filter (fun a ↦ ¬p a)).prod = s.prod := by rw [← prod_add, filter_add_not]

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