proposition: Lemma zero_dimension_prod (I : choiceType) (T : I -> topologicalType) : (forall i, zero_dimensional (T i)) -> zero_dimensional (prod_topology T).
proof: Proof. move=> dctTI x y /eqP xneqy. have [i/eqP/dctTI [U [clU Ux nUy]]] : exists i, x i <> y i. by apply/existsNP=> W; exact/xneqy/functional_extensionality_dep. exists (proj i @^-1` U); split => //; apply: clopen_comp => //. 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