From da06f0bee1217bdeb7ecd6fdf30ce07ae6373387 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Sat, 29 Nov 2025 00:44:22 +0900 Subject: [PATCH 1/3] adherence value, extracted seq, limit point --- CHANGELOG_UNRELEASED.md | 9 ++ reals/reals.v | 12 ++ theories/normedtype_theory/normed_module.v | 8 ++ theories/sequences.v | 158 +++++++++++++++++++++ 4 files changed, 187 insertions(+) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 5ee0ae5bbd..4fdb7ae90d 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -88,6 +88,15 @@ + lemma `open_subball_rat` + fact `isolated_rat_ball` + lemma `countable_isolated` +- in `normed_module.v`: + + lemma `limit_point_setD` + +- in `reals.v`: + + lemma `nat_has_minimum` + +- in `sequences.v`: + + definition `adherence_value` + + lemmas `adherence_value_cvg`, `limit_point_adherence_value` ### Changed diff --git a/reals/reals.v b/reals/reals.v index 842399f50b..b334ebb650 100644 --- a/reals/reals.v +++ b/reals/reals.v @@ -656,6 +656,18 @@ rewrite (le_trans _ (lbBi _ Bk)) //. by move/negP : i1x; rewrite -ltNge ltzD1. Qed. +Lemma nat_has_minimum (A : set nat) : A !=set0 -> + exists j, A j /\ forall k, A k -> (j <= k)%N. +Proof. +move=> A0. +pose B : set int := [set x%:~R | x in A]. +have B0 : B !=set0 by case: A0 => a Aa; exists a%:~R, a. +have : lbound B 0 by move=> _ [b0 Bb0 <-]; rewrite ler0z. +move/(int_lbound_has_minimum B0) => [_ [[i Ai <-]]] Bi. +exists i; split => // k Bk. +by have := Bi k%:~R; rewrite ler_int; apply; exists k. +Qed. + Section rat_in_itvoo. Let bound_div (R : archiRealFieldType) (x y : R) : nat := diff --git a/theories/normedtype_theory/normed_module.v b/theories/normedtype_theory/normed_module.v index 61055e4269..e938cb24a2 100644 --- a/theories/normedtype_theory/normed_module.v +++ b/theories/normedtype_theory/normed_module.v @@ -1096,6 +1096,14 @@ move=> p q _ _ /=; apply: contraPP => /eqP. by rewrite neq_lt => /orP[] /arv /[swap] ->; rewrite ltxx. Qed. +Lemma limit_point_setD {R : archiRealFieldType} (A V : set R) a : + finite_set V -> limit_point A a -> limit_point (A `\` V) a. +Proof. +move=> finV /limit_point_infinite_setP aA. +apply/limit_point_infinite_setP => U aU. +by rewrite setIDA; apply: infinite_setD => //; exact: aA. +Qed. + Lemma EFin_lim (R : realFieldType) (f : nat -> R) : cvgn f -> limn (EFin \o f) = (limn f)%:E. Proof. diff --git a/theories/sequences.v b/theories/sequences.v index 4283d85cb1..5998a5fb21 100644 --- a/theories/sequences.v +++ b/theories/sequences.v @@ -57,6 +57,7 @@ From mathcomp Require Import ereal topology tvs normedtype landau. (* is convergent and its limit is sup u_n *) (* nonincreasing_cvgn u_ == if u_ is nonincreasing u_ and bound by below *) (* then u_ is convergent *) +(* adherence_value u_ a == a is an adherence value of the sequence u_ *) (* adjacent_seq == adjacent sequences lemma *) (* cesaro == Cesaro's lemma *) (* ``` *) @@ -2671,6 +2672,163 @@ apply: nondecreasing_cvgn_le; last exact: is_cvg_geometric_series. by apply: nondecreasing_series => ? _ /=; rewrite pmulr_lge0 // exprn_gt0. Qed. +Definition adherence_value {R : numDomainType} (u_ : R^nat) (a : R) := + forall (e : R) n, e > 0 -> exists2 p, (p >= n)%N & `|u_ p - a| <= e. + +Section adherence_value_cvg. +Context {R : realType}. +Variables (u_ : R^nat) (a : R). + +(* We build a sequence of increasing positive indices N_k s.t. + |u_N_k - a| <= 1/k where N_k is the smallest natural number of the set + A(N, k) defined below. *) + +Let A N k := [set j | (j > N)%N /\ `|u_ j - a| <= k.+1%:R^-1]. + +Let elt_prop Nk := + [/\ `|u_ Nk.1 - a| <= Nk.2%:R^-1, A Nk.1 Nk.2 !=set0 & (0 < Nk.2)%N]. + +Let elt_type := {x : nat * nat | elt_prop x}. + +Let N_ (x : elt_type) := (proj1_sig x).1. + +Let idx_ (x : elt_type) := (proj1_sig x).2. + +Let N_idx x : `|u_ (N_ x) - a| <= (idx_ x)%:R^-1. +Proof. by move: x => [[? ?]] []. Qed. + +Let A_nonempty x : A (N_ x) (idx_ x) !=set0. +Proof. by move: x => [[? ?]] []. Qed. + +Let elt_rel i j := [/\ idx_ j = (idx_ i).+1, + (N_ j > N_ i)%N & N_ j = proj1_sig (cid (nat_has_minimum (A_nonempty i)))]. + +Let N_incr v k p : (forall n, elt_rel (v n) (v n.+1)) -> + (k < p)%N -> (N_ (v k) < N_ (v p))%N. +Proof. +move=> vrel kp. +have {}Nv n : (N_ (v n) < N_ (v n.+1))%O by have [_] := vrel n. +by move/increasing_seqP/leqW_mono : Nv => ->. +Qed. + +Let idx_incr v n : (forall n, elt_rel (v n) (v n.+1)) -> (n <= idx_ (v n))%N. +Proof. +by move=> vrel; elim: n => // n /leq_ltn_trans; apply; have [->] := vrel n. +Qed. + +Let adherence_value_cvg_direct : adherence_value u_ a -> + exists2 f : nat -> nat, increasing_seq f & u_ \o f @ \oo --> a. +Proof. +move=> u_a. +have [N0 N01] : {N0 | `| u_ N0 - a | <= 1^-1}. + by move: u_a => /(_ 1 1 ltr01)/cid2[N1 _] N1a1; exists N1; rewrite invr1. +have A0 : A N0 1 !=set0. + move: u_a => /(_ 2^-1 N0.+1). + by rewrite invr_gt0// ltr0n => /(_ isT)[j N0j j1]; exists j. +have [v [v0 vrel]] : {v : nat -> elt_type | + v 0 = exist elt_prop (N0, 1) (And3 N01 A0 isT) /\ + forall n, elt_rel (v n) (v n.+1) }. + apply: dependent_choice => // -[[N i] /=] [uNi ANi0 i0]. + pose M := proj1_sig (cid (nat_has_minimum ANi0)). + have Mi1 : `|u_ M - a| <= i.+1%:R^-1 by rewrite /M; case: cid => /= x [[]]. + have AMi1 : A M i.+1 !=set0. + move: u_a => /(_ i.+2%:R^-1 M.+1). + by rewrite invr_gt0// ltr0n => /(_ isT)/cid2[m nm um]; exists m. + exists (exist elt_prop (M, i.+1) (And3 Mi1 AMi1 isT)). + rewrite /elt_rel/= /N_/=; split; first exact. + - by rewrite /M; case: cid => // x [[]]. + - rewrite /M; case: cid => // x [/= ANix ANi]. + case: cid => //= y [/ANi xy] /(_ _ ANix) yx. + by apply/eqP; rewrite eq_le leEnat xy yx. +exists (N_ \o v \o S). + by apply/increasing_seqP => n; exact: N_incr. +apply/subr_cvg0/cvgrPdist_le => /= e e0; near=> n. +rewrite sub0r normrN (le_trans (N_idx (v n.+1)))//. +rewrite invf_ple ?posrE//; last by rewrite ltr0n; case: (v n.+1) => -[? ?] []. +rewrite (@le_trans _ _ n.+1%:R)//; last by rewrite ler_nat idx_incr. +by rewrite -nat1r -lerBlDl; near: n; exact: nbhs_infty_ger. +Unshelve. all: end_near. Qed. + +Lemma adherence_value_cvg : adherence_value u_ a <-> + exists2 f : nat -> nat, increasing_seq f & (u_ \o f @ \oo --> a). +Proof. +split => // -[f incrf] /cvgrPdist_le/= + e n e0. +move=> /(_ _ e0)[N _ {}Nauf]. +exists (f (n + N)); last by rewrite distrC Nauf//= leq_addl. +rewrite (@leq_trans (f n))//. + elim: n => // n; rewrite -ltnS => /leq_trans; apply. + by move/increasing_seqP : incrf; exact. +by rewrite -leEnat incrf leq_addr. +Qed. + +Lemma limit_point_adherence_value : + limit_point (range u_) a -> adherence_value u_ a. +Proof. +pose U := range u_. +pose V i := [set u_ k | k in `I_i]. +have finV i : finite_set (V i) by exact/finite_image/finite_II. +(* we pick up elements u_N_k from the following set: *) +pose aU k := `]a - k.+1%:R^-1, a + k.+1%:R^-1[ `&` ((U `\` V k) `\ a). +move=> u_a. +have aU0 k : aU k !=set0. + have /(limit_pointP _ _).1 [a_ [au a_a]] := limit_point_setD (finV k) u_a. + move/cvgrPdist_lt => /(_ k.+1%:R^-1). + rewrite invr_gt0 ltr0n => /(_ isT)[N _ a_cvg]. + exists (a_ N); split; first by rewrite /= in_itv/= -ltr_distlC a_cvg/=. + split; last exact/eqP. + split; first by have /au[] := imageT a_ N. + by case => x xk uxaN; have /au[_] := imageT a_ N; apply => /=; exists x. +have idx_aU k : exists N1, u_ N1 \in aU k. + have [/= y [/= a1y [[[m _ umy] Uny] ya]]] := aU0 k. + exists m; rewrite inE /aU umy; split => //=; split => //; split => //. + by exists m. +have [N0 N01] : {N0 | `| u_ N0 - a | <= 1^-1}. + apply/cid; have [a_ [au a_a]] := (limit_pointP _ _).1 u_a. + move/cvgrPdist_le => /(_ _ ltr01)[N _] /(_ _ (leqnn N)) aaN1. + have /au[x _ uxaN] := imageT a_ N. + by exists x; rewrite uxaN distrC invr1. +have A0 : A N0 1 !=set0. + have [N1] := idx_aU N0.+1. + rewrite inE => -[/= uN1 [[[x _ uxuN1] /= VN0N1] uN1_a]]. + exists x; split. + by rewrite ltnNge; apply/negP => xN0; apply: VN0N1; exists x. + move: uN1; rewrite in_itv/= -ltr_distlC uxuN1 distrC => /ltW/le_trans; apply. + by rewrite lef_pV2 ?posrE// ler_nat. +have [v [v0 vrel]] : {v : nat -> elt_type | + v 0%N = exist elt_prop (N0, 1) (And3 N01 A0 isT) /\ + forall n, elt_rel (v n) (v n.+1) }. + apply: dependent_choice => // -[[N i] /=] [uNi ANi0 i0]. + pose M := proj1_sig (cid (nat_has_minimum ANi0)). + have M0 : (0 < M)%N. + by rewrite /M; case: cid => //= x [[+ _] _]; exact: leq_trans. + have Mi1 : `|u_ M - a| <= i.+1%:R^-1 by rewrite /M; case: cid => /= x [[]]. + have AMi1 : A M i.+1 !=set0. + have [N1] := idx_aU (maxn i.+1 M.+1). + rewrite inE => -[/= uN1 [[[x _ uxuN2] /= Vi1M1] uN1_a]]. + have Mx : (M < x)%N. + rewrite ltnNge; apply/negP => xM. + by apply: Vi1M1; exists x => //; rewrite /(`I_ _) leq_max !ltnS xM orbT. + exists x; split => //. + move: uN1; rewrite in_itv -ltr_distlC uxuN2 distrC => /ltW/le_trans; apply. + by rewrite lef_pV2 ?posrE// ler_nat ltnS leq_max ltnSn. + exists (exist elt_prop (M, i.+1) (And3 Mi1 AMi1 isT)). + rewrite /elt_rel/= /N_/=; split; first exact. + - by rewrite /M; case: cid => // x [[]]. + - rewrite /M; case: cid => // x [ANix ANi]/=. + case: cid => //= y; rewrite /idx_/= => -[/ANi xy /(_ _ ANix) yx]. + by apply/eqP; rewrite eq_le leEnat xy yx. +apply/adherence_value_cvg; exists (N_ \o v). + by apply/increasing_seqP => n; exact: N_incr. +apply/cvgrPdist_le => /= e e0; near=> n. +have := N_idx (v n); rewrite distrC => /le_trans; apply. +rewrite invf_ple//; last first. + by rewrite posrE ltr0n; case: (v n) => [[? ?] []]. +rewrite (@le_trans _ _ n%:R)//; last by rewrite ler_nat idx_incr. +by near: n; exact: nbhs_infty_ger. +Unshelve. all: end_near. Qed. + +End adherence_value_cvg. + Section adjacent_cut. Context {R : realType}. Implicit Types L D E : set R. From 60822ca452d9476b585c1a2f3823fc9c9aff9308 Mon Sep 17 00:00:00 2001 From: affeldt-aist <33154536+affeldt-aist@users.noreply.github.com> Date: Thu, 4 Dec 2025 11:08:43 +0900 Subject: [PATCH 2/3] Update reals/reals.v Co-authored-by: Quentin VERMANDE --- reals/reals.v | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/reals/reals.v b/reals/reals.v index b334ebb650..fee962db81 100644 --- a/reals/reals.v +++ b/reals/reals.v @@ -661,10 +661,10 @@ Lemma nat_has_minimum (A : set nat) : A !=set0 -> Proof. move=> A0. pose B : set int := [set x%:~R | x in A]. -have B0 : B !=set0 by case: A0 => a Aa; exists a%:~R, a. -have : lbound B 0 by move=> _ [b0 Bb0 <-]; rewrite ler0z. +have B0 : B !=set0 by apply: image_nonempty. +have: lbound B 0 by move=> _ [b0 Bb0 <-]; rewrite ler0z. move/(int_lbound_has_minimum B0) => [_ [[i Ai <-]]] Bi. -exists i; split => // k Bk. +exists i; split=> // k Bk. by have := Bi k%:~R; rewrite ler_int; apply; exists k. Qed. From 93b45897bfb4a298afe5f3c6c6e4aec5046382d1 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Mon, 15 Dec 2025 09:22:58 +0900 Subject: [PATCH 3/3] use cluster for adherence values of a sequence Co-authored-by: Cyril Cohen --- CHANGELOG_UNRELEASED.md | 4 +-- theories/sequences.v | 62 ++++++++++++++++++++++++++--------------- 2 files changed, 41 insertions(+), 25 deletions(-) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 4fdb7ae90d..4991a2ebac 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -95,8 +95,8 @@ + lemma `nat_has_minimum` - in `sequences.v`: - + definition `adherence_value` - + lemmas `adherence_value_cvg`, `limit_point_adherence_value` + + lemma `cluster_eventuallyP` + + lemmas `cluster_eventually_cvg`, `limit_point_cluster_eventually` ### Changed diff --git a/theories/sequences.v b/theories/sequences.v index 5998a5fb21..1140cf3bff 100644 --- a/theories/sequences.v +++ b/theories/sequences.v @@ -57,7 +57,6 @@ From mathcomp Require Import ereal topology tvs normedtype landau. (* is convergent and its limit is sup u_n *) (* nonincreasing_cvgn u_ == if u_ is nonincreasing u_ and bound by below *) (* then u_ is convergent *) -(* adherence_value u_ a == a is an adherence value of the sequence u_ *) (* adjacent_seq == adjacent sequences lemma *) (* cesaro == Cesaro's lemma *) (* ``` *) @@ -2672,10 +2671,26 @@ apply: nondecreasing_cvgn_le; last exact: is_cvg_geometric_series. by apply: nondecreasing_series => ? _ /=; rewrite pmulr_lge0 // exprn_gt0. Qed. -Definition adherence_value {R : numDomainType} (u_ : R^nat) (a : R) := - forall (e : R) n, e > 0 -> exists2 p, (p >= n)%N & `|u_ p - a| <= e. +(* adherence values of a sequence *) +Lemma cluster_eventuallyP {R : realFieldType} (u_ : R^nat) (a : R) : + cluster (u_ @ \oo) a <-> + forall (e : R) n, e > 0 -> exists2 p, (p >= n)%N & `|a - u_ p| <= e. +Proof. +split => [/= uya e n e0|u_a /= A B [n/= _ nuA] [e/= e0 aeB]]. +- apply/not_exists2P => nuae. + have yuAe : nbhs \oo (u_ @^-1` [set x | `|a - x| > e]). + exists n => // m/= nm; have := nuae m. + by rewrite nm/= => -[//|/negP]; rewrite -ltNge. + have [/= r []] := uya _ _ yuAe (nbhsx_ballx a _ e0). + by rewrite /ball/= => /ltW; rewrite leNgt => /negbTE ->. +- have e20 : 0 < e / 2 by rewrite divr_gt0. + have [p np upae] := u_a _ n e20. + exists (u_ p); split; first exact: nuA. + apply: aeB => /=. + by rewrite (le_lt_trans upae)// gtr_pMr// invf_lt1// ltr1n. +Qed. -Section adherence_value_cvg. +Section cluster_eventually_cvg. Context {R : realType}. Variables (u_ : R^nat) (a : R). @@ -2683,10 +2698,10 @@ Variables (u_ : R^nat) (a : R). |u_N_k - a| <= 1/k where N_k is the smallest natural number of the set A(N, k) defined below. *) -Let A N k := [set j | (j > N)%N /\ `|u_ j - a| <= k.+1%:R^-1]. +Let A N k := [set j | (j > N)%N /\ `|a - u_ j| <= k.+1%:R^-1]. Let elt_prop Nk := - [/\ `|u_ Nk.1 - a| <= Nk.2%:R^-1, A Nk.1 Nk.2 !=set0 & (0 < Nk.2)%N]. + [/\ `|a - u_ Nk.1| <= Nk.2%:R^-1, A Nk.1 Nk.2 !=set0 & (0 < Nk.2)%N]. Let elt_type := {x : nat * nat | elt_prop x}. @@ -2694,7 +2709,7 @@ Let N_ (x : elt_type) := (proj1_sig x).1. Let idx_ (x : elt_type) := (proj1_sig x).2. -Let N_idx x : `|u_ (N_ x) - a| <= (idx_ x)%:R^-1. +Let N_idx x : `|a - u_ (N_ x)| <= (idx_ x)%:R^-1. Proof. by move: x => [[? ?]] []. Qed. Let A_nonempty x : A (N_ x) (idx_ x) !=set0. @@ -2716,11 +2731,11 @@ Proof. by move=> vrel; elim: n => // n /leq_ltn_trans; apply; have [->] := vrel n. Qed. -Let adherence_value_cvg_direct : adherence_value u_ a -> +Let cluster_eventually_cvg_direct : cluster (u_ @ \oo) a -> exists2 f : nat -> nat, increasing_seq f & u_ \o f @ \oo --> a. Proof. -move=> u_a. -have [N0 N01] : {N0 | `| u_ N0 - a | <= 1^-1}. +move=> /cluster_eventuallyP u_a. +have [N0 N01] : {N0 | `| a - u_ N0 | <= 1^-1}. by move: u_a => /(_ 1 1 ltr01)/cid2[N1 _] N1a1; exists N1; rewrite invr1. have A0 : A N0 1 !=set0. move: u_a => /(_ 2^-1 N0.+1). @@ -2730,7 +2745,7 @@ have [v [v0 vrel]] : {v : nat -> elt_type | forall n, elt_rel (v n) (v n.+1) }. apply: dependent_choice => // -[[N i] /=] [uNi ANi0 i0]. pose M := proj1_sig (cid (nat_has_minimum ANi0)). - have Mi1 : `|u_ M - a| <= i.+1%:R^-1 by rewrite /M; case: cid => /= x [[]]. + have Mi1 : `|a - u_ M| <= i.+1%:R^-1 by rewrite /M; case: cid => /= x [[]]. have AMi1 : A M i.+1 !=set0. move: u_a => /(_ i.+2%:R^-1 M.+1). by rewrite invr_gt0// ltr0n => /(_ isT)/cid2[m nm um]; exists m. @@ -2743,26 +2758,27 @@ have [v [v0 vrel]] : {v : nat -> elt_type | exists (N_ \o v \o S). by apply/increasing_seqP => n; exact: N_incr. apply/subr_cvg0/cvgrPdist_le => /= e e0; near=> n. -rewrite sub0r normrN (le_trans (N_idx (v n.+1)))//. +rewrite sub0r normrN distrC (le_trans (N_idx (v n.+1)))//. rewrite invf_ple ?posrE//; last by rewrite ltr0n; case: (v n.+1) => -[? ?] []. rewrite (@le_trans _ _ n.+1%:R)//; last by rewrite ler_nat idx_incr. by rewrite -nat1r -lerBlDl; near: n; exact: nbhs_infty_ger. Unshelve. all: end_near. Qed. -Lemma adherence_value_cvg : adherence_value u_ a <-> +Lemma cluster_eventually_cvg : cluster (u_ @ \oo) a <-> exists2 f : nat -> nat, increasing_seq f & (u_ \o f @ \oo --> a). Proof. -split => // -[f incrf] /cvgrPdist_le/= + e n e0. -move=> /(_ _ e0)[N _ {}Nauf]. -exists (f (n + N)); last by rewrite distrC Nauf//= leq_addl. +split => // -[f incrf] /cvgrPdist_le/= auf. +apply/cluster_eventuallyP => e n e0; move: auf. +move=> /(_ _ e0)[N _ {}Nauf]. +exists (f (n + N)); last by rewrite Nauf//= leq_addl. rewrite (@leq_trans (f n))//. elim: n => // n; rewrite -ltnS => /leq_trans; apply. by move/increasing_seqP : incrf; exact. by rewrite -leEnat incrf leq_addr. Qed. -Lemma limit_point_adherence_value : - limit_point (range u_) a -> adherence_value u_ a. +Lemma limit_point_cluster_eventually : + limit_point (range u_) a -> cluster (u_ @ \oo) a. Proof. pose U := range u_. pose V i := [set u_ k | k in `I_i]. @@ -2782,11 +2798,11 @@ have idx_aU k : exists N1, u_ N1 \in aU k. have [/= y [/= a1y [[[m _ umy] Uny] ya]]] := aU0 k. exists m; rewrite inE /aU umy; split => //=; split => //; split => //. by exists m. -have [N0 N01] : {N0 | `| u_ N0 - a | <= 1^-1}. +have [N0 N01] : {N0 | `| a - u_ N0 | <= 1^-1}. apply/cid; have [a_ [au a_a]] := (limit_pointP _ _).1 u_a. move/cvgrPdist_le => /(_ _ ltr01)[N _] /(_ _ (leqnn N)) aaN1. have /au[x _ uxaN] := imageT a_ N. - by exists x; rewrite uxaN distrC invr1. + by exists x; rewrite uxaN invr1. have A0 : A N0 1 !=set0. have [N1] := idx_aU N0.+1. rewrite inE => -[/= uN1 [[[x _ uxuN1] /= VN0N1] uN1_a]]. @@ -2801,7 +2817,7 @@ have [v [v0 vrel]] : {v : nat -> elt_type | pose M := proj1_sig (cid (nat_has_minimum ANi0)). have M0 : (0 < M)%N. by rewrite /M; case: cid => //= x [[+ _] _]; exact: leq_trans. - have Mi1 : `|u_ M - a| <= i.+1%:R^-1 by rewrite /M; case: cid => /= x [[]]. + have Mi1 : `|a - u_ M| <= i.+1%:R^-1 by rewrite /M; case: cid => /= x [[]]. have AMi1 : A M i.+1 !=set0. have [N1] := idx_aU (maxn i.+1 M.+1). rewrite inE => -[/= uN1 [[[x _ uxuN2] /= Vi1M1] uN1_a]]. @@ -2817,7 +2833,7 @@ have [v [v0 vrel]] : {v : nat -> elt_type | - rewrite /M; case: cid => // x [ANix ANi]/=. case: cid => //= y; rewrite /idx_/= => -[/ANi xy /(_ _ ANix) yx]. by apply/eqP; rewrite eq_le leEnat xy yx. -apply/adherence_value_cvg; exists (N_ \o v). +apply/cluster_eventually_cvg; exists (N_ \o v). by apply/increasing_seqP => n; exact: N_incr. apply/cvgrPdist_le => /= e e0; near=> n. have := N_idx (v n); rewrite distrC => /le_trans; apply. @@ -2827,7 +2843,7 @@ rewrite (@le_trans _ _ n%:R)//; last by rewrite ler_nat idx_incr. by near: n; exact: nbhs_infty_ger. Unshelve. all: end_near. Qed. -End adherence_value_cvg. +End cluster_eventually_cvg. Section adjacent_cut. Context {R : realType}.