|
Lemma eq_eseries (R : realFieldType) (f g : (\bar R)^nat) (P : pred nat) : |
|
(forall i, P i -> f i = g i) -> \sum_(i <oo | P i) f i = \sum_(i <oo | P i) g i. |
|
Proof. by move=> efg; congr (lim _); apply/funext => n; exact: eq_bigr. Qed. |
maybe with should be eq_eseriesr
