Adjoining one point to the condition of a filtered product #
Weakening the condition P of a filtered product over s to P i ∨ i = c, for a point c
with ¬P c, multiplies the product by the factor at c exactly when c ∈ s. This is the
bookkeeping that adds a closed endpoint to a sum over the points of a finite set in an open
interval.
Main results #
Finset.prod_filter_or_eq_of_not,Finset.sum_filter_or_eq_of_not: adjoining one point to the condition of a filtered product or sum.
theorem
Finset.prod_filter_or_eq_of_not
{ι : Type u_1}
{M : Type u_2}
[DecidableEq ι]
[CommMonoid M]
(s : Finset ι)
(f : ι → M)
(P : ι → Prop)
[DecidablePred P]
{c : ι}
(hc : ¬P c)
:
Adjoining a point c with ¬P c to the condition P of a filtered product over s
multiplies it by the factor at c exactly when c ∈ s.
theorem
Finset.sum_filter_or_eq_of_not
{ι : Type u_1}
{M : Type u_2}
[DecidableEq ι]
[AddCommMonoid M]
(s : Finset ι)
(f : ι → M)
(P : ι → Prop)
[DecidablePred P]
{c : ι}
(hc : ¬P c)
:
Adjoining a point c with ¬P c to the condition P of a filtered sum over
s adds the term at c exactly when c ∈ s.