fact: Definition compact_openK_nbhs (f : compact_openK) := filter_from [set O | f @` K `<=` O /\ open O] (fun O => [set g | g @` K `<=` O]).
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap generic_quotient) mathcomp(boolp classical_sets functions) mathcomp(cardinality mathcomp_extra fsbigop) reals signed