proposition: Lemma limit_pointEnbhs E : limit_point E = [set p | globally (E `\ p) `#` nbhs p].
proof: Proof. under eq_fun do rewrite meets_globallyl; rewrite funeqE => p /=. apply/eq_forall2 => x px; apply/eq_exists => y. by rewrite propeqE; split => [[/eqP ? ?]|[[? /eqP ?]]]; do 2?split. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap generic_quotient) mathcomp(boolp classical_sets functions) mathcomp(cardinality mathcomp_extra fsbigop) reals signed