proposition: Lemma join_product_continuous : continuous join_product.
proof: Proof. suff : continuous (join_product : weakT -> PU). by move=> cts x U => /cts; rewrite nbhs_simpl /= -weak_sep_nbhsE. move=> x; apply/cvg_sup; first exact/fmap_filter/(nbhs_filter (x : weakT)). move=> i; move: x; apply/(@continuousP _ (weak_topology (@^~ i))) => A [B ? E]. rewrite -E (_ : @^~ i = proj i) //. have -> : join_product @^-1` (proj i @^-1` B) = f_ i @^-1` B by []. apply: open_comp => // + _; rewrite /cvg_to => x U. by rewrite nbhs_simpl /= -weak_sep_nbhsE; move: x U; exact: ctsf. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap generic_quotient) mathcomp(boolp classical_sets functions) mathcomp(cardinality mathcomp_extra fsbigop) reals signed