proposition: Lemma rV_compact (T : topologicalType) n (A : 'I_n.+1 -> set T) : (forall i, compact (A i)) -> compact [ set v : 'rV[T]_n.+1 | forall i, A i (v ord0 i)].
proof: Proof. move=> Aico. have : @compact (prod_topology _) [set f | forall i, A i (f i)]. by apply: tychonoff. move=> Aco F FF FA. set G := [set [set f : 'I_n.+1 -> T | B (\row_j f j)] | B in F]. have row_simpl (v : 'rV[T]_n.+1) : \row_j (v ord0 j) = v. by apply/rowP => ?; rewrite mxE. have row_simpl' (f : 'I_n.+1 -> T) : (\row_j f j) ord0 = f. by rewrite funeqE=> ?; rewrite mxE. have [f [Af clGf]] : [set f | forall i, A i (f i)] `&` @cluster (prod_topology _) G !=set0. suff GF : ProperFilter G. apply: Aco; exists [set v : 'rV[T]_n.+1 | forall i, A i (v ord0 i)] => //. by rewrite predeqE => f; split => Af i; [have := Af i|]; rewrite row_simpl'. apply Build_ProperFilter. move=> _ [C FC <-]; have /filter_ex [v Cv] := FC. by exists (v ord0); rewrite /= row_simpl. split. - by exists setT => //; apply: filterT. - by move=> _ _ [C FC <-] [D FD <-]; exists (C `&` D) => //; apply: filterI. move=> C D sCD [E FE EeqC]; exists [set v : 'rV[T]_n.+1 | D (v ord0)]. by apply: filterS FE => v Ev; apply/sCD; rewrite -EeqC/= row_simpl. by rewrite predeqE => ? /=; rewrite row_simpl'. exists (\row_j f j); split; first by move=> i; rewrite mxE; apply: Af. move=> C D FC f_D; have {}f_D : nbhs (f : prod_topology _) [set g | D (\row_j g j)]. have [E f_E sED] := f_D; rewrite nbhsE. set Pj := fun j Bj => open_nbhs (f j) Bj /\ Bj `<=` E ord0 j. have exPj : forall j, exists Bj, open_nbhs (f j) Bj /\ Bj `<=` E ord0 j. move=> j; have := f_E ord0 j; rewrite nbhsE => - [Bj]. by rewrite row_simpl'; exists Bj. exists [set g | forall j, (get (Pj j)) (g j)]; last first. move=> g Pg; apply: sED => i j; rewrite ord1 row_simpl'. by have /getPex [_ /(_ _ (Pg j))] := exPj j. split; last by move=> j; have /getPex [[]] := exPj j. exists [set [set g | forall j, get (Pj j) (g j)] | k in [set x | 'I_n.+1 x]]; last first. rewrite predeqE => g; split; first by move=> [_ [_ _ <-]]. move=> Pg; exists [set g | forall j, get (Pj j) (g j)] => //. by exists ord0. move=> _ [_ _ <-]; set s := [seq (@^~ j) @^-1` (get (Pj j)) | j : 'I_n.+1]. exists [fset x in s]%fset. move=> B'; rewrite in_fset => /mapP [j _ ->]; rewrite inE. exists j => //; exists (get (Pj j)) => //. by have /getPex [[]] := exPj j. rewrite predeqE => g; split=> [Ig j|Ig B']. apply: (Ig ((@^~ j) @^-1` (get (Pj j)))). by rewrite /= in_fset; apply/mapP; exists j => //; rewrite mem_enum. by rewrite /= in_fset => /mapP [j _ ->]; apply: Ig. have GC : G [set g | C (\row_j g j)] by exists C. by have [g []] := clGf _ _ GC f_D; exists (\row_j (g j : T)). Qed.
imports: HB(structures) mathcomp(all_ssreflect ssralg ssrint ssrnum finmap matrix) mathcomp(rat interval zmodp vector fieldext falgebra) mathcomp(mathcomp_extra boolp classical_sets functions) mathcomp(cardinality set_interval Rstruct) ereal reals signed topology prodnormedzmodule