proposition: Lemma compact_openK_nbhsE_subproof (p : compact_openK) : compact_openK_nbhs p = [set A | exists B : set compact_openK, [/\ compact_open_of_nbhs B, B p & B `<=` A]].
proof: Proof. rewrite eqEsubset; split => A /=. case=> B /= [fKB oB gKBA]; exists [set g | g @` K `<=` B]; split => //. by move=> h /= hKB; exists B. by case=> B [oB Bf /filterS]; apply; exact: oB. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap generic_quotient) mathcomp(boolp classical_sets functions) mathcomp(cardinality mathcomp_extra fsbigop) reals signed