proposition: Lemma totally_disconnected_prod (I : choiceType) (T : I -> topologicalType) (A : forall i, set (T i)) : (forall i, totally_disconnected (A i)) -> @totally_disconnected (prod_topology T) (fun f => forall i, A i (f i)).
proof: Proof. move=> dsctAi x /= Aix; rewrite eqEsubset; split; last first. by move=> ? ->; exact: connected_component_refl. move=> f /= [C /= [Cx CA ctC Cf]]; apply/functional_extensionality_dep => i. suff : proj i @` C `<=` [set x i] by apply; exists f. rewrite -(dsctAi i) // => Ti ?; exists (proj i @` C) => //. split; [by exists x | by move=> ? [r Cr <-]; exact: CA |]. apply/(connected_continuous_connected ctC)/continuous_subspaceT. 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