proposition: Lemma proj_continuous i : continuous (proj i : prod_topology K -> K i).
proof: Proof. move=> f; have /cvg_sup/(_ i)/cvg_image : f --> f by apply: cvg_id. move=> h; apply: cvg_trans (h _) => {h}. by move=> Q /= [W nbdW <-]; apply: filterS nbdW; exact: preimage_image. rewrite eqEsubset; split => y //; exists (dfwith (fun=> point) i y) => //. by rewrite dfwithin. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap generic_quotient) mathcomp(boolp classical_sets functions) mathcomp(cardinality mathcomp_extra fsbigop) reals signed