proposition: Lemma sup_ent_split A : sup_ent A -> exists2 B, sup_ent B & B \; B `<=` A.
proof: Proof. have spt : (forall ie : IEnt, ent_of ((projT1 ie).1, ((@split_ent (TS (projT1 ie).1) (projT1 ie).2)))). by case=> [[/= ??] /asboolP/entourage_split_ent ?]; exact/asboolP. pose g : (IEnt -> IEnt) := fun x => exist ent_of _ (spt x). case => W [F _ <-] sA; exists (\bigcap_(x in [set` F]) (projT1 (g x)).2). exists (\bigcap_(ie in [set`F]) (projT1 (g ie)).2) => //. exists [fset (g ie) | ie in F]%fset; first by move=> /= ??; exact: in_setT. rewrite eqEsubset; split; case=> x y Igxy ie. by move => ?; apply/(Igxy (g ie))/imfsetP; exists ie. by move=> /imfsetP [?? ->]; exact: Igxy. case => ?? [z Fxz Fzy]; apply: sA; IEntP=> i e ? ? eF. apply: ((@entourage_split (TS i)) z) => //. exact: (Fxz _ eF). exact: (Fzy _ eF). Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap generic_quotient) mathcomp(boolp classical_sets functions) mathcomp(cardinality mathcomp_extra fsbigop) reals signed