Helper

bigD1_filter

File dumas2017dual/lib/extra_algebra.v

Section bigop_extra

Type Lemma

Proof Lines 6

Signature

Lemma bigD1_filter {R : Type} {op : SemiGroup.com_law R} {idx : R} {I : eqType} (r : seq I) (j : I) (P : pred I) (F : I -> R) : j \in r -> P j -> uniq r -> \big[op/idx]_(i <- [seq x <- r | P x]) F i = op (F j) (\big[op/idx]_(i <- [seq x <- r | P x] | i != j) F i).

Description

Extract a term from a filtered big operation: if j is in r and satisfies P, we can factor out F(j) from the sum/product over filtered elements. Useful for manipulating sums over constrained index sets.

Uses (0)

This lemma does not use any other lemmas from the stats.

Used By (0)

No lemmas in the stats use this lemma.

Coq Source Code

View on GitHub

Loading source code...

← Back to Stats