proposition: Lemma pointwise_precompact_equicontinuous (W : set (X -> Y)) : pointwise_precompact W id -> equicontinuous W id -> precompact (W : set {family compact, X -> Y }).
proof: Proof. move=> /pointwise_precompact_precompact + ectsW. rewrite ?precompactE compact_ultra compact_ultra pointwise_compact_closure //. move=> /= + F UF FcW => /(_ F UF); rewrite image_id => /(_ FcW)[p [cWp Fp]]. exists p; split => //; apply/pointwise_compact_cvg => //. apply/near_powerset_filter_fromP; first exact: equicontinuous_subset_id. exists (closure (W : set {ptws X -> Y })) => //. exact: equicontinuous_closure. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap generic_quotient) mathcomp(boolp classical_sets functions) mathcomp(cardinality mathcomp_extra fsbigop) reals signed