proposition: Lemma pointwise_compact_closure (W : set (X -> Y)) : equicontinuous W id -> closure (W : set {family compact, X -> Y}) = closure (W : set {ptws X -> Y}).
proof: Proof. rewrite ?closureEcvg // predeqE => ? ?. split; move=> [F PF [Fx WF]]; (exists F; last split) => //. apply/@pointwise_compact_cvg => //; apply/near_powerset_filter_fromP. exact: equicontinuous_subset_id. by exists W => //; exact: WF. apply/@pointwise_compact_cvg => //; apply/near_powerset_filter_fromP. exact: equicontinuous_subset_id. by exists W => //; exact: WF. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap generic_quotient) mathcomp(boolp classical_sets functions) mathcomp(cardinality mathcomp_extra fsbigop) reals signed