proposition: Lemma sup_ent_nbhs : @nbhs Tt Tt = nbhs_ sup_ent.
proof: Proof. rewrite predeq2E => x V; split. move=> [/= X [[/= B + <-] [W BW Wx BV]]] => /(_ W BW) [] /=. move=> F Fsup Weq; move: Weq Wx BW => <- Fx BF. case (pselect ([set: I] = set0)) => [I0 | /eqP/set0P [i0 _]]. suff -> : V = setT by exists setT; apply: filterT; exact: sup_ent_filter. rewrite -subTset => ??; apply: BV; exists (\bigcap_(i in [set` F]) i) => //. by move=> w /Fsup/set_mem; rewrite /sup_subbase I0 bigcup_set0. have f : forall w, {p : IEnt | w \in F -> to_set ((projT1 p).2) x `<=` w}. move=> /= v; apply: cid; case (pselect (v \in F)); first last. by move=> ?; exists (exist ent_of _ (IEnt_pointT i0)). move=> /[dup] /Fx vx /Fsup/set_mem [i _]; rewrite openE => /(_ x vx). by move=> /(@nbhsP (TS i)) [w /asboolP ent ?]; exists (exist _ (i, w) ent). exists (\bigcap_(w in [set` F]) (projT1 (projT1 (f w))).2); first last. move=> v /= Fgw; apply: BV; exists (\bigcap_(i in [set` F]) i) => //. by move=> w /[dup] ? /Fgw /= /(projT2 (f w)); exact. exists (\bigcap_(w in [set` F]) (projT1 (projT1 (f w))).2) => //. exists [fset (fun i => (projT1 (f i))) w | w in F]%fset. by move=> u ?; exact: in_setT. rewrite eqEsubset; split => y + z. by move=>/(_ (projT1 (f z))) => + ?; apply; apply/imfsetP; exists z. by move=> Fgy /imfsetP [/= u uF ->]; exact: Fgy. case=> E [D [/= F FsubEnt <-] FsubE EsubV]. have F_nbhs_x: Filter (nbhs x) by typeclasses eauto. apply: (filterS EsubV). pose f : IEnt -> set T := fun w => @interior (TS (projT1 w).1) (to_set ((projT1 w).2) (x)). exists (\bigcap_(w in [set` F]) f w); repeat split. - exists [set \bigcap_(w in [set` F]) f w]; last by rewrite bigcup_set1. move=> ? ->; exists [fset f w | w in F]%fset. move=> /= ? /imfsetP [[[/= i w /[dup] /asboolP entw ? Fiw ->]]]. by apply/mem_set; rewrite /f /=; exists i => //; exact: open_interior. by rewrite set_imfset bigcap_image //=. - by IEntP=> ? ? /open_nbhs_entourage entw ??; apply entw. - by move=> t /= Ifwt; apply: FsubE => it /Ifwt/interior_subset. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap generic_quotient) mathcomp(boolp classical_sets functions) mathcomp(cardinality mathcomp_extra fsbigop) reals signed