proposition: Lemma fam_cvgP (fam : set U -> Prop) (F : set_system (U -> V)) (f : U -> V) : Filter F -> {family fam, F --> f} <-> (forall A : set U, fam A -> {uniform A, F --> f }).
proof: Proof. split; first by move=> /cvg_sup + A FA; move/(_ (existT _ _ FA)). by move=> famFf /=; apply/cvg_sup => [[? ?] FA]; apply: famFf. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap generic_quotient) mathcomp(boolp classical_sets functions) mathcomp(cardinality mathcomp_extra fsbigop) reals signed