proposition: Lemma cvg_sup (F : set_system T) (t : T) : Filter F -> F --> (t : S) <-> forall i, F --> (t : TS i).
proof: Proof. move=> Ffilt; split=> cvFt. move=> i A /=; rewrite (@nbhsE (TS i)) => - [B [Bop Bt] sBA]. apply: cvFt; exists B; split=> //; exists [set B]; last first. by rewrite predeqE => ?; split=> [[_ ->]|] //; exists B. move=> _ ->; exists [fset B]%fset. by move=> ?; rewrite inE inE => /eqP->; exists i. by rewrite predeqE=> ?; split=> [|??]; [apply|]; rewrite /= inE // =>/eqP->. move=> A /=; rewrite (@nbhsE [the topologicalType of S]). move=> [_ [[B sB <-] [C BC Ct] sUBA]]. rewrite nbhs_filterE; apply: filterS sUBA _; apply: (@filterS _ _ _ C). by move=> ? ?; exists C. have /sB [D sD IDeC] := BC; rewrite -IDeC; apply: filter_bigI => E DE. have /sD := DE; rewrite inE => - [i _]; rewrite openE => Eop. by apply: (cvFt i); apply: Eop; move: Ct; rewrite -IDeC => /(_ _ DE). Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap generic_quotient) mathcomp(boolp classical_sets functions) mathcomp(cardinality mathcomp_extra fsbigop) reals signed