proposition: Lemma uniform_pointwise_compact (W : set (X -> Y)) : compact (W : set (@uniform_fun_family X Y compact)) -> compact (W : set {ptws X -> Y}).
proof: Proof. rewrite [x in x _ -> _]compact_ultra [x in _ -> x _]compact_ultra. move=> + F UF FW => /(_ F UF FW) [h [Wh Fh]]; exists h; split => //. by move=> Q Fq; apply: (pointwise_cvg_compact_family _ Fh). Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap generic_quotient) mathcomp(boolp classical_sets functions) mathcomp(cardinality mathcomp_extra fsbigop) reals signed