proposition: Lemma weak_ent_nbhs : nbhs = nbhs_ weak_ent.
proof: Proof. rewrite predeq2E => x V; split. case=> [? [[B ? <-] ? BsubV]]; have: nbhs (f x) B by apply: open_nbhs_nbhs. move=> /nbhsP [W ? WsubB]; exists ((map_pair f) @^-1` W); first by exists W. by move=>??; exact/BsubV/WsubB. case=> W [V' entV' V'subW] /filterS; apply. have : nbhs (f x) to_set V' (f x) by apply/nbhsP; exists V'. rewrite (@nbhsE U) => [[O [openU Ofx Osub]]]. (exists (f @^-1` O); repeat split => //); first by exists O => //. by move=> w ? ; apply: V'subW; exact: Osub. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap generic_quotient) mathcomp(boolp classical_sets functions) mathcomp(cardinality mathcomp_extra fsbigop) reals signed