proposition: Lemma tychonoff (I : eqType) (T : I -> topologicalType) (A : forall i, set (T i)) : (forall i, compact (A i)) -> compact [set f : prod_topology T | forall i, A i (f i)].
proof: Proof. move=> Aco; rewrite compact_ultra => F FU FA. set subst_coord := fun (i : I) (pi : T i) (f : forall x : I, T x) (j : I) => if eqP is ReflectT e then ecast i (T i) (esym e) pi else f j. have subst_coordT i pi f : subst_coord i pi f i = pi. rewrite /subst_coord; case eqP => // e. by rewrite (eq_irrelevance e (erefl _)). have subst_coordN i pi f j : i != j -> subst_coord i pi f j = f j. move=> inej; rewrite /subst_coord; case: eqP => // e. by move: inej; rewrite {1}e => /negP. have pr_surj i : @^~ i @` [set: forall i, T i] = setT. rewrite predeqE => pi; split=> // _. by exists (subst_coord i pi (fun _ => point))=> //; rewrite subst_coordT. pose pF i : set_system _ := [set @^~ i @` B | B in F]. have pFultra : forall i, UltraFilter (pF i). by move=> i; apply: ultra_image (pr_surj i). have pFA : forall i, pF i (A i). move=> i; exists [set g | forall i, A i (g i)] => //. rewrite predeqE => pi; split; first by move=> [g Ag <-]; apply: Ag. move=> Aipi; have [f Af] := filter_ex FA. exists (subst_coord i pi f); last exact: subst_coordT. move=> j; case: (eqVneq i j); first by case: _ /; rewrite subst_coordT. by move=> /subst_coordN ->; apply: Af. have cvpFA i : A i `&` [set p | pF i --> p] !=set0. by rewrite -ultra_cvg_clusterE; apply: Aco. exists (fun i => get (A i `&` [set p | pF i --> p])). split=> [i|]; first by have /getPex [] := cvpFA i. by apply/cvg_sup => i; apply/cvg_image=> //; have /getPex [] := cvpFA i. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap generic_quotient) mathcomp(boolp classical_sets functions) mathcomp(cardinality mathcomp_extra fsbigop) reals signed