proposition: Lemma precompact_equicontinuous (W : set {family compact, X -> Y}) : (forall f, W f -> continuous f) -> precompact (W : set {family compact, X -> Y}) -> equicontinuous W id.
proof: Proof. move=> pcptW ctsW; apply: (equicontinuous_subset_id (@subset_closure _ W)). apply: compact_equicontinuous; last by rewrite -precompactE. move=> f; rewrite closureEcvg => [[G PG [Gf GW]]] x B /=. rewrite -nbhs_entourageE => -[E entE] /filterS; apply; near_simpl. suff ctsf : continuous f by move: E entE; apply/cvg_app_entourageP; exact: ctsf. apply/continuous_localP => x'; apply/near_powerset_filter_fromP. by move=> ? ?; exact: continuous_subspaceW. case: (@lcptX x') => // U; rewrite withinET => nbhsU [cptU _]. exists U => //; apply: (uniform_limit_continuous_subspace PG _ _). by near=> g; apply: continuous_subspaceT; near: g; exact: GW. by move/fam_cvgP/(_ _ cptU) : Gf. Unshelve. 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