proposition: Lemma family_cvg_finite_covers (famA famB : set U -> Prop) (F : set_system (U -> V)) (f : U -> V) : Filter F -> (forall P, famA P -> exists (I : choiceType) f, (forall i, famB (f i)) /\ finite_subset_cover [set: I] f P) -> {family famB, F --> f} -> {family famA, F --> f}.
proof: Proof. move=> FF ex_finCover /fam_cvgP rFf; apply/fam_cvgP => A famAA. move: ex_finCover => /(_ _ famAA) [R [g [g_famB [D _]]]]. move/uniform_subset_cvg; apply. elim/finSet_rect: D => X IHX. have [->|/set0P[x xX]] := eqVneq [set` X] set0. by rewrite coverE bigcup_set0; apply: cvg_uniform_set0. rewrite coverE (bigcup_fsetD1 x)//; apply: cvg_uniformU. exact/rFf/g_famB. exact/IHX/fproperD1. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap generic_quotient) mathcomp(boolp classical_sets functions) mathcomp(cardinality mathcomp_extra fsbigop) reals signed