proposition: Lemma join_product_open (A : set T) : open A -> open ((join_product @` A) : set (subspace (range join_product))).
proof: Proof. move=> oA; rewrite openE => y /= [x Ax] jxy. have [// | i nAfiy] := @sepf (~` A) x (open_closedC oA). pose B : set PU := proj i @^-1` (~` closure (f_ i @` ~` A)). apply: (@filterS _ _ _ (range join_product `&` B)). move=> z [[w ?]] wzE Bz; exists w => //. move: Bz; rewrite /B -wzE closureC; case=> K [oK KsubA] /KsubA. have -> : proj i (join_product w) = f_ i w by []. by move=> /exists2P/forallNP/(_ w)/not_andP [] // /contrapT. apply: open_nbhs_nbhs; split; last by rewrite -jxy. apply: openI; first exact: open_subspaceT. apply: open_subspaceW; apply: open_comp; last exact/closed_openC/closed_closure. by move=> + _; exact: proj_continuous. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap generic_quotient) mathcomp(boolp classical_sets functions) mathcomp(cardinality mathcomp_extra fsbigop) reals signed