proposition: Lemma compact_open_open (K : set T) (O : set U) : compact K -> open O -> open ([set g | g @` K `<=` O] : set compact_open).
proof: Proof. pose C := [set g | g @` K `<=` O]; move=> cptK oO. exists [set C]; last by rewrite bigcup_set1. move=> _ ->; exists (fset1 C) => //; last by rewrite set_fset1 bigcap_set1. by move=> _ /[!inE] ->; exists (existT _ _ cptK) => // z Cz; exists O. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap generic_quotient) mathcomp(boolp classical_sets functions) mathcomp(cardinality mathcomp_extra fsbigop) reals signed