proposition: Lemma equicontinuous_closure (W : set {ptws X -> Y}) : equicontinuous W id -> equicontinuous (closure W) id.
proof: Proof. move=> ectsW => x E entE; near=> y => f clWf. near (within W (nbhs (f : {ptws X -> Y}))) => g. near: g; rewrite near_withinE; near_simpl; near=> g => Wg. apply: (@entourage_split _ (g x)) => //. exact: (near (pointwise_cvg_entourage _ _ _)). apply: (@entourage_split _ (g y)) => //; first exact: (near (@ectsW x _ _)). by apply/entourage_sym; exact: (near (pointwise_cvg_entourage _ _ _)). Unshelve. all: by 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