proposition: Lemma cvgi_lim {U} {F} {FF : ProperFilter F} (f : U -> T -> Prop) (l : T) : F (fun x : U => is_subset1 (f x)) -> f `@ F --> l -> lim (f `@ F) = l.
proof: Proof. move=> f_prop fl; apply: get_unique => // l' fl'; exact: cvgi_unique _ fl' fl. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap generic_quotient) mathcomp(boolp classical_sets functions) mathcomp(cardinality mathcomp_extra fsbigop) reals signed