proposition: Lemma hausdorff_product : (forall x, hausdorff_space (K x)) -> hausdorff_space (prod_topology K).
proof: Proof. move=> hsdfK p q /= clstr; apply: functional_extensionality_dep => x. apply: hsdfK; move: clstr; rewrite ?cluster_cvgE /= => -[G PG [GtoQ psubG]]. exists (proj x @ G); [exact: fmap_proper_filter|split]. apply: cvg_trans; last exact: (@proj_continuous x q). by apply: cvg_app; exact: GtoQ. move/(cvg_app (proj x)): psubG => /cvg_trans; apply. 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