proposition: Lemma countable_sup_ent : countable [set: Ii] -> (forall n, countable_uniformity (TS n)) -> countable_uniformity Tt.
proof: Proof. move=> Icnt countable_ent; pose f n := cid (countable_ent n). pose g (n : Ii) : set (set (T * T)) := projT1 (f n). have [I0 | /set0P [i0 _]] := eqVneq [set: I] set0. exists [set setT]; split; [exact: countable1|move=> A ->; exact: entourageT|]. move=> P [w [A _]] <- subP; exists setT => //. apply: subset_trans subP; apply: sub_bigcap => i _ ? _. by suff : [set: I] (projT1 i).1 by rewrite I0. exists (finI_from (\bigcup_n g n) id); split. - by apply/finI_from_countable/bigcup_countable => //i _; case: (projT2 (f i)). - move=> E [A AsubGn AE]; exists E => //. have h (w : set (T * T)) : { p : IEnt | w \in A -> w = (projT1 p).2 }. apply: cid; have [|] := boolP (w \in A); last first. by exists (exist ent_of _ (IEnt_pointT i0)). move=> /[dup] /AsubGn /set_mem [n _ gnw] wA. suff ent : ent_of (n, w) by exists (exist ent_of (n, w) ent). by apply/asboolP; have [_ + _] := projT2 (f n); exact. exists [fset sval (h w) | w in A]%fset; first by move=> ?; exact: in_setT. rewrite -AE; rewrite eqEsubset; split => t Ia. by move=> w Aw; rewrite (svalP (h w) Aw); apply/Ia/imfsetP; exists w. case=> [[n w]] p /imfsetP [x /= xA M]; apply: Ia. by rewrite (_ : w = x) // (svalP (h x) xA) -M. - move=> E [w] [ A _ wIA wsubE]. have ent_Ip (i : IEnt) : @entourage (TS (projT1 i).1) (projT1 i).2. by apply/asboolP; exact: (projT2 i). pose h (i : IEnt) : {x : set (T * T) | _} := cid2 (and3_rec (fun _ _ P => P) (projT2 (f (projT1 i).1)) (projT1 i).2 (ent_Ip i)). have ehi (i : IEnt) : ent_of ((projT1 i).1, projT1 (h i)). apply/asboolP => /=; have [] := projT2 (h i). by have [_ + _ ? ?] := projT2 (f (projT1 i).1); exact. pose AH := [fset projT1 (h w) | w in A]%fset. exists (\bigcap_(i in [set` AH]) i). exists AH => // p /imfsetP [i iA ->]; rewrite inE //. by exists (projT1 i).1 => //; have [] := projT2 (h i). apply: subset_trans wsubE; rewrite -wIA => ? It i ?. by have [?] := projT2 (h i); apply; apply: It; apply/imfsetP; exists 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