proposition: Lemma set_nbhsP (B : set T) : set_nbhs B <-> (exists C, [/\ open C, A `<=` C & C `<=` B]).
proof: Proof. split; first last. by case=> V [? AV /filterS +] x /AV ?; apply; apply: open_nbhs_nbhs. move=> snB; have Ux x : exists U, A x -> [/\ U x, open U & U `<=` B]. have [/snB|?] := pselect (A x); last by exists point. by rewrite nbhsE => -[V [? ? ?]]; exists V. exists (\bigcup_(x in A) (projT1 (cid (Ux x)))); split. - by apply: bigcup_open => x Ax; have [] := projT2 (cid (Ux x)). - by move=> x Ax; exists x => //; have [] := projT2 (cid (Ux x)). - by move=> x [y Ay]; have [//| _ _] := projT2 (cid (Ux y)); exact. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap generic_quotient) mathcomp(boolp classical_sets functions) mathcomp(cardinality mathcomp_extra fsbigop) reals signed