proposition: Lemma perfect_prod {I : Type} (i : I) (K : I -> topologicalType) : perfect_set [set: K i] -> perfect_set [set: prod_topology K].
proof: Proof. move=> /perfectTP KPo; apply/perfectTP => f oF; apply: (KPo (f i)). rewrite (_ : [set f i] = proj i @` [set f]). by apply: (@proj_open {classic I} _ i); exact: oF. by rewrite eqEsubset; split => ? //; [move=> -> /=; exists f | case=> g ->]. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap generic_quotient) mathcomp(boolp classical_sets functions) mathcomp(cardinality mathcomp_extra fsbigop) reals signed