proposition: Lemma compact_cvg_within_compact {U : topologicalType} {V : uniformType} (C : set U) (F : set_system (U -> V)) (f : U -> V) : Filter F -> compact C -> {uniform C, F --> f} <-> {family compactly_in C, F --> f}.
proof: Proof. move=> FF CC. apply: (iff_trans _ (iff_sym (fam_cvgP _ _ FF))); split. - by move=> CFf D [/uniform_subset_cvg + _]; apply. - by apply; split. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap generic_quotient) mathcomp(boolp classical_sets functions) mathcomp(cardinality mathcomp_extra fsbigop) reals signed