proposition: Lemma proj_open i (A : set (prod_topology K)) : open A -> open (proj i @` A).
proof: Proof. move=> oA; rewrite openE => z [f Af <-]; rewrite openE in oA. have {oA} := oA _ Af; rewrite /interior => nAf. apply: (@filterS _ _ _ ((dfwith f i) @^-1` A)). by move=> w Apw; exists (dfwith f i w) => //; rewrite projK. apply: dfwith_continuous => /=; move: nAf; congr (nbhs _ A). by apply: functional_extensionality_dep => ?; case: dfwithP. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap generic_quotient) mathcomp(boolp classical_sets functions) mathcomp(cardinality mathcomp_extra fsbigop) reals signed