proposition: Lemma cvg_closeP (F : set_system U) (l : U) : ProperFilter F -> F --> l <-> ([cvg F in U] /\ close (lim F) l).
proof: Proof. move=> FF; split=> [Fl|[cvF]Cl]. by have /cvgP := Fl; split=> //; apply: (@cvg_close _ F). by apply: cvg_trans (close_cvgxx Cl). Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap generic_quotient) mathcomp(boolp classical_sets functions) mathcomp(cardinality mathcomp_extra fsbigop) reals signed