proposition: Lemma family_cvg_subset (famA famB : set U -> Prop) (F : set_system (U -> V)) (f : U -> V) : Filter F -> famA `<=` famB -> {family famB, F --> f} -> {family famA, F --> f}.
proof: Proof. by move=> FF S /fam_cvgP famBFf; apply/fam_cvgP => A ?; apply/famBFf/S. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap generic_quotient) mathcomp(boolp classical_sets functions) mathcomp(cardinality mathcomp_extra fsbigop) reals signed