fact: Definition limit_point E := [set t : T | forall U, nbhs t U -> exists y, [/\ y != t, E y & U y]].
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap generic_quotient) mathcomp(boolp classical_sets functions) mathcomp(cardinality mathcomp_extra fsbigop) reals signed