proposition: Lemma cvgi_unique {U : Type} {F} {FF : ProperFilter F} (f : U -> set T) : {near F, is_fun f} -> is_subset1 [set x : T | f `@ F --> x].
proof: Proof. by move=> ffun fx fy; rewrite -closeE //; exact: cvgi_close. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap generic_quotient) mathcomp(boolp classical_sets functions) mathcomp(cardinality mathcomp_extra fsbigop) reals signed