proposition: Lemma join_product_weak : set_inj [set: T] join_product -> @open T = @open (weak_topology join_product).
proof: Proof. move=> inj; rewrite predeqE => U; split; first last. by move=> [V ? <-]; apply: open_comp => // + _; exact: join_product_continuous. move=> /join_product_open/open_subspaceP [V [oU VU]]. exists V => //; have := @f_equal _ _ (preimage join_product) _ _ VU. rewrite !preimage_setI // !preimage_range !setIT => ->. rewrite eqEsubset; split; last exact: preimage_image. by move=> z [w Uw] /inj <- //; rewrite inE. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap generic_quotient) mathcomp(boolp classical_sets functions) mathcomp(cardinality mathcomp_extra fsbigop) reals signed