proposition: Lemma cvgi_close T' {F} {FF : ProperFilter F} (f : T' -> set T) (l l' : T) : {near F, is_fun f} -> f `@ F --> l -> f `@ F --> l' -> close l l'.
proof: Proof. move=> f_prop fFl fFl'. suff f_totalfun: infer {near F, is_totalfun f} by exact: cvg_close fFl fFl'. apply: filter_app f_prop; near do split=> //=. have: (f `@ F) setT by apply: fFl; apply: filterT. by rewrite fmapiE; apply: filterS => x [y []]; exists y. Unshelve. all: by 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