set of limit points is closed

[affeldt-aist]

Motivation for this change

This standard lemma about limit points was missing and was found useful in another development by @IshiguroYoshihiro

Checklist

• added corresponding entries in CHANGELOG_UNRELEASED.md

- [ ] added corresponding documentation in the headers

Reference: How to document

Merge policy

As a rule of thumb:

• PRs with several commits that make sense individually and that
  all compile are preferentially merged into master.
• PRs with disorganized commits are very likely to be squash-rebased.

Reminder to reviewers

• Read this Checklist
• Put a milestone if possible
• Check labels

[t6s]

The proved result can be (at least) generalized to T1:

Section limit_point_closed.
Context {T : topologicalType}.
Implicit Types (A : set T) (a : T).

Lemma not_limit_point_set1 A a : ~ limit_point A a ->
  exists X : set T, nbhs a X /\ A `&` X `<=` [set a].
Proof.
rewrite /limit_point/=.
move=> /existsNP[] X /not_implyP[] naX /forallNP H.
exists X; split => // x/= [] Ax Xx; have := H x.
by move=> /not_and3P[]// /negP; rewrite negbK => /eqP.
Qed.

Lemma limit_pointPn A a : ~ limit_point A a <->
  (exists X : set T, nbhs a X /\ A `&` X `<=` [set a]).
Proof.
split; first exact: not_limit_point_set1.
case=> X [] XaX AXa.
rewrite /limit_point/= -existsNE.
exists X; apply/not_implyP; split => //.
case=> x [] + ? ? => /eqP; apply.
by apply: AXa; split.
Qed.

Lemma limit_point_closed A : accessible_space T -> closed (limit_point A).
Proof.
move=> ?.
rewrite -openC openE/= => a /not_limit_point_set1[]X[].
rewrite nbhsE/= => -[]U oaU UX XAa.
rewrite /interior nbhsE/=.
exists U => // x Ux.
apply/limit_pointPn.
have [xa|xneqa] := eqVneq x a.
  exists U; rewrite xa; split; first exact: open_nbhs_nbhs.
  by apply: (@subset_trans _ (A `&` X)) => //; exact: setIS.
exists (U `&` [set~ a]); split.
  apply: open_nbhs_nbhs; split.
    apply: openI; first by case: oaU.
    by rewrite openC; exact: accessible_closed_set1.
  by split => //; exact/eqP.
apply: (@subset_trans _ (A `&` (X `&` [set~ a]))).
  by apply: setIS; apply: setSI.
apply: (@subset_trans _ ([set a] `&` [set~ a])).
  by rewrite setIA; apply: setSI.
by rewrite setICr.
Qed.

End limit_point_closed.
Arguments limit_point_closed {T} A.

[t6s]

limit_pointsPn can also be like this:

Lemma limit_pointNE A a : (~ limit_point A a) =
  (exists X : set T, nbhs a X /\ A `&` X `<=` [set a]).
Proof.
rewrite /limit_point/= -existsNE; apply: eq_exists => X/=.
rewrite not_implyE; congr and.
rewrite -forallNE; apply: eq_forall => x/=.
rewrite and3E not_andE orC -implyE; congr (_ -> _).
by rewrite -(propext (rwP negP)) not_notE -(propext (rwP eqP)).
Qed.

[t6s]

(limit_pointEn? I don't know the appropriate naming convention here)

[affeldt-aist]

(limit_pointEn? I don't know the appropriate naming convention here)

Maybe not_limit_pointE?