proposition: Lemma closure_limit_point E : closure E = E `|` limit_point E.
proof: Proof. rewrite predeqE => t; split => [cEt|]; last first. by case; [exact: subset_closure|exact: subset_limit_point]. have [?|Et] := pselect (E t); [by left|right=> U tU; have [p []] := cEt _ tU]. by exists p; split => //; apply/eqP => pt; apply: Et; rewrite -pt. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap generic_quotient) mathcomp(boolp classical_sets functions) mathcomp(cardinality mathcomp_extra fsbigop) reals signed