proposition: Lemma closedE : closed = [set A : set T | forall p, ~ (\near p, ~ A p) -> A p].
proof: Proof. rewrite predeqE => A; split=> Acl p; last first. by move=> clAp; apply: Acl; rewrite -nbhs_nearE => /clAp [? []]. rewrite -nbhs_nearE nbhsE => /asboolP. rewrite asbool_neg => /forallp_asboolPn2 clAp. apply: Acl => B; rewrite nbhsE => - [C [oC pC]]. have /asboolP := clAp C. rewrite asbool_or 2!asbool_neg => /orP[/asboolP/not_andP[]//|/existsp_asboolPn [q]]. move/asboolP; rewrite asbool_neg => /imply_asboolPn[+ /contrapT Aq sCB] => /sCB. by exists q. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap generic_quotient) mathcomp(boolp classical_sets functions) mathcomp(cardinality mathcomp_extra fsbigop) reals signed