fact: Definition nbhs_of_open (T : Type) (op : set T -> Prop) (p : T) (A : set T) := exists B, [/\ op B, B p & B `<=` A].
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap generic_quotient) mathcomp(boolp classical_sets functions) mathcomp(cardinality mathcomp_extra fsbigop) reals signed