proposition: Lemma limit_pointEonbhs E : limit_point E = [set p | globally (E `\ p) `#` open_nbhs p].
proof: Proof. by rewrite limit_pointEnbhs; under eq_fun do rewrite meets_openr. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap generic_quotient) mathcomp(boolp classical_sets functions) mathcomp(cardinality mathcomp_extra fsbigop) reals signed