proposition: Lemma cvg_unique {F} {FF : ProperFilter F} : is_subset1 [set x : T | F --> x].
proof: Proof. move=> Fx Fy; rewrite -closeE //; exact: (@cvg_close F). Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap generic_quotient) mathcomp(boolp classical_sets functions) mathcomp(cardinality mathcomp_extra fsbigop) reals signed