proposition: Lemma equicontinuous_continuous {I} (W : set I) (fW : I -> (X -> Y)) (i : I) : equicontinuous W fW -> W i -> continuous (fW i).
proof: Proof. move=> ectsW Wf x; apply: equicontinuous_continuous_for; last exact: Wf. by move=> ?; exact: ectsW. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap generic_quotient) mathcomp(boolp classical_sets functions) mathcomp(cardinality mathcomp_extra fsbigop) reals signed