proposition: Lemma discrete_cvg (F : set_system X) (x : X) : Filter F -> F --> x <-> F [set x].
proof: Proof. rewrite dsc nbhs_simpl; split; first by exact. by move=> Fx U /principal_filterP ?; apply: filterS Fx => ? ->. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap generic_quotient) mathcomp(boolp classical_sets functions) mathcomp(cardinality mathcomp_extra fsbigop) reals signed