proposition: Lemma limit_pointP (T : archiFieldType) (A : set T) (x : T) : limit_point A x <-> exists a_ : nat -> T, [/\ a_ @` setT `<=` A, forall n, a_ n != x & a_ @ \oo --> x].
proof: Proof. split=> [Ax|[a_ [aTA a_x] ax]]; last first. move=> U /ax[m _ a_U]; near \oo => n; exists (a_ n); split => //. by apply aTA; exists n. by apply a_U; near: n; exists m. pose U := fun n : nat => [set z : T | `|x - z| < n.+1%:R^-1]. suff /(_ _)/cid-/all_sig[a_ anx] : forall n, exists a, a != x /\ (U n `&` A) a. exists a_; split. - by move=> a [n _ <-]; have [? []] := anx n. - by move=> n; have [] := anx n. - apply/cvgrPdist_lt => _/posnumP[e]; near=> n; have [? [] Uan Aan] := anx n. by rewrite (lt_le_trans Uan)// ltW//; near: n; exact: near_infty_natSinv_lt. move=> n; have : nbhs (x : T) (U n). by apply/(nbhs_ballP (x:T) (U n)); rewrite nbhs_ballE; exists n.+1%:R^-1 => //=. by move/Ax/cid => [/= an [anx Aan Uan]]; exists an. Unshelve. all: by end_near. Qed.
imports: HB(structures) mathcomp(all_ssreflect ssralg ssrint ssrnum finmap matrix) mathcomp(rat interval zmodp vector fieldext falgebra) mathcomp(mathcomp_extra boolp classical_sets functions) mathcomp(cardinality set_interval Rstruct) ereal reals signed topology prodnormedzmodule