proposition: Lemma notbig_family_sum a f: infinite_c a -> (cardinal (domain f)) <=c a -> (forall i, inc i (domain f) -> (Vg f i) <=c a) -> (csum f) <=c a.
proof: Proof. move=> ifa leda alea. set (g:= cst_graph (domain f) a). have dg : domain f = domain g by rewrite /g Lgd. have ale: forall x, inc x (domain f) -> (Vg f x) <=c (Vg g x). by move=> x xdf; rewrite /g LgV//; apply: alea. move: (cprod_inf1 leda ifa) (csum_increasing dg ale). rewrite [csum g]csum_of_same cprod2cr => r1 r2; apply: cleT r2 r1. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)