proposition: Lemma limg_bigcap f I r (P : pred I) Us : (f @: (\bigcap_(i <- r | P i) Us i) <= \bigcap_(i <- r | P i) f @: Us i)%VS.
proof: Proof. elim/big_rec2: _ => [|i V U _ sUV]; first exact: subvf. by rewrite (subv_trans (limg_cap f _ U)) ?capvS. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop finfun tuple) mathcomp(ssralg matrix mxalgebra zmodp)