proposition: Lemma snd_open {U V : topologicalType} (A : set (U * V)) : open A -> open (snd @` A).
proof: Proof. rewrite !openE => oA z [[a b/=] Aab <-]; rewrite /interior. have [[P Q] [Pa Qb] pqA] := oA _ Aab; apply: (@filterS _ _ _ Q) => // q Qq. by exists (a, q) => //=; apply: pqA; split => //; exact: nbhs_singleton. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap generic_quotient) mathcomp(boolp classical_sets functions) mathcomp(cardinality mathcomp_extra fsbigop) reals signed