proposition: Lemma compact_open_cvgP (F : set_system compact_open) (f : compact_open) : Filter F -> F --> f <-> forall K O, @compact T K -> @open U O -> f @` K `<=` O -> F [set g | g @` K `<=` O].
proof: Proof. move=> FF; split. by move/cvg_sup => + K O cptK ? ? => /(_ (existT _ _ cptK)); apply; exists O. move=> fko; apply/cvg_sup => -[A cptK] O /= [C /= [fAC oC]]. by move/filterS; apply; exact: fko. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap generic_quotient) mathcomp(boolp classical_sets functions) mathcomp(cardinality mathcomp_extra fsbigop) reals signed