Helper

bigD1_seq_cond

File dumas2017dual/lib/extra_algebra.v

Section bigop_extra

Type Lemma

Proof Lines 10

Signature

Lemma bigD1_seq_cond {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 <- r | P i) F i = op (F j) (\big[op/idx]_(i <- r | P i && (i != j)) F i).

Description

Extract a term from a conditional big operation over a sequence. Similar to bigD1 but for conditional sums: factors out F(j) when j satisfies P, leaving the rest with an additional (i != j) condition.

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