proposition: Lemma closed_cvg {T} {V : topologicalType} {F} {FF : ProperFilter F} (u_ : T -> V) (A : V -> Prop) : closed A -> (\forall n \near F, A (u_ n)) -> forall l, u_ @ F --> l -> A l.
proof: Proof. move=> + FAu_ l u_Fl; apply => B /u_Fl /=; rewrite nbhs_filterE. by move=> /(filterI FAu_) => /filter_ex[t [Au_t u_Bt]]; exists (u_ t). Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap generic_quotient) mathcomp(boolp classical_sets functions) mathcomp(cardinality mathcomp_extra fsbigop) reals signed