proposition: Lemma closureC E : ~` closure E = \bigcup_(x in [set U | open U /\ U `<=` ~` E]) x.
proof: Proof. rewrite closureE setC_bigcap eqEsubset; split => t [U [? EU Ut]]. by exists (~` U) => //; split; [exact: closed_openC|exact: subsetC]. by rewrite -(setCK E); exists (~` U)=> //; split; [exact:open_closedC|exact:subsetC]. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap generic_quotient) mathcomp(boolp classical_sets functions) mathcomp(cardinality mathcomp_extra fsbigop) reals signed