From 79e6f9d18133164f6e7286eef9ec607bbb784793 Mon Sep 17 00:00:00 2001 From: zstone Date: Fri, 20 Sep 2024 22:24:11 -0400 Subject: [PATCH] change in nat topology --- theories/sequences.v | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/theories/sequences.v b/theories/sequences.v index 5a54e2407a..b12c952168 100644 --- a/theories/sequences.v +++ b/theories/sequences.v @@ -1370,9 +1370,9 @@ Lemma cvg_nseries_near (u : nat^nat) : cvgn (nseries u) -> \forall n \near \oo, u n = 0%N. Proof. move=> /cvg_ex[l ul]; have /ul[a _ aul] : nbhs l [set l]. - by exists [set l]; split=> //; exists [set l] => //; rewrite bigcup_set1. + by rewrite nbhs_principalE. have /ul[b _ bul] : nbhs l [set l.-1; l]. - by exists [set l]; split => //; exists [set l] => //; rewrite bigcup_set1. + by rewrite nbhs_principalE ; apply/principal_filterP => /=; right. exists (maxn a b) => // n /= abn. rewrite (_ : u = fun n => nseries u n.+1 - nseries u n)%N; last first. by rewrite funeqE => i; rewrite /nseries big_nat_recr//= addnC addnK.