proposition: Lemma equicontinuous_subset {I J} (W : set I) (V : set J) {fW : I -> X -> Y} {fV : J -> X -> Y} : fW @`W `<=` fV @` V -> equicontinuous V fV -> equicontinuous W fW.
proof: Proof. move=> WsubV + x E entE => /(_ x E entE); apply: filterS => y VE i Wi. by case: (WsubV (fW i)); [exists i | move=> j Vj <-; exact: VE]. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap generic_quotient) mathcomp(boolp classical_sets functions) mathcomp(cardinality mathcomp_extra fsbigop) reals signed