From 9bc55550d1c76fc1e219ce6d7b714790fa0b3f1e 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 056cc7d073..c2da0ea093 100644 --- a/theories/sequences.v +++ b/theories/sequences.v @@ -1377,9 +1377,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.