proposition: Lemma equicontinuous_continuous_for {I} (W : set I) (fW : I -> X -> Y) i x : {for x, equicontinuous W fW} -> W i -> {for x, continuous (fW i)}.
proof: Proof. move=> ectsW Wf; apply/cvg_entourageP => E entE; near_simpl. by near=> y; apply: (near (ectsW _ entE) y). Unshelve. end_near. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap generic_quotient) mathcomp(boolp classical_sets functions) mathcomp(cardinality mathcomp_extra fsbigop) reals signed