proposition: Lemma dnbhsE (T : topologicalType) (x : T) : nbhs x = x^' `&` at_point x.
proof: Proof. rewrite predeqE => A; split=> [x_A|[x_A Ax]]. split; last exact: nbhs_singleton. move: x_A; rewrite nbhsE => -[B [oB x_B sBA]]; rewrite /dnbhs nbhsE. by exists B => // ? /sBA. move: x_A; rewrite /dnbhs !nbhsE => -[B [oB x_B sBA]]; exists B => //. by move=> y /sBA Ay; case: (eqVneq y x) => [->|]. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap generic_quotient) mathcomp(boolp classical_sets functions) mathcomp(cardinality mathcomp_extra fsbigop) reals signed