proposition: Lemma weak_sep_cvg (F : set_system T) (x : T) : Filter F -> (F --> (x : T)) <-> (F --> (x : weakT)).
proof: Proof. move=> FF; split. move=> FTx; apply/cvg_sup => i U. have /= -> := @nbhsE (weak_topology (f_ i)) x. case=> B [[C oC <- ?]] /filterS; apply; apply: FTx; rewrite /= nbhsE. by exists (f_ i @^-1` C) => //; split => //; exact: open_comp. move/cvg_sup => wiFx U; rewrite /= nbhs_simpl nbhsE => [[B [oB ?]]]. move/filterS; apply; have [//|i nclfix] := @sepf _ x (open_closedC oB). apply: (wiFx i); have /= -> := @nbhsE (weak_topology (f_ i)) x. exists (f_ i @^-1` (~` closure [set f_ i x | x in ~` B])); [split=>//|]. apply: open_comp; last by rewrite ?openC; last apply: closed_closure. by move=> + _; exact: (@weak_continuous _ _ (f_ i)). rewrite closureC preimage_bigcup => z [V [oV]] VnB => /VnB. by move/forall2NP => /(_ z) [] // /contrapT. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap generic_quotient) mathcomp(boolp classical_sets functions) mathcomp(cardinality mathcomp_extra fsbigop) reals signed