fact: Definition equicontinuous {I} (W : set I) (d : I -> (X -> Y)) := forall x (E : set (Y * Y)), entourage E -> \forall y \near x, forall i, W i -> E (d i x, d i y).
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap generic_quotient) mathcomp(boolp classical_sets functions) mathcomp(cardinality mathcomp_extra fsbigop) reals signed