proposition: Lemma cvg_image (F : set_system S) (s : S) : Filter F -> f @` setT = setT -> F --> (s : W) <-> ([set f @` A | A in F] : set_system _) --> f s.
proof: Proof. move=> FF fsurj; split=> [cvFs|cvfFfs]. move=> A /weak_continuous [B [Bop Bs sBAf]]. have /cvFs FB : nbhs (s : W) B by apply: open_nbhs_nbhs. rewrite nbhs_simpl; exists (f @^-1` A); first exact: filterS FB. exact: image_preimage. move=> A /= [_ [[B Bop <-] Bfs sBfA]]. have /cvfFfs [C FC fCeB] : nbhs (f s) B by rewrite nbhsE; exists B. rewrite nbhs_filterE; apply: filterS FC. by apply: subset_trans sBfA; rewrite -fCeB; apply: preimage_image. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap generic_quotient) mathcomp(boolp classical_sets functions) mathcomp(cardinality mathcomp_extra fsbigop) reals signed