fact: Definition product_topology_def := sup_topology (fun i => Topological.class (weak_topology (fun f : [the pointedType of (forall i : I, T i)] => f i))).
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap generic_quotient) mathcomp(boolp classical_sets functions) mathcomp(cardinality mathcomp_extra fsbigop) reals signed