From fa2bfc678063419a0fdfa246f462f1629d1f69f4 Mon Sep 17 00:00:00 2001 From: affeldt-aist <33154536+affeldt-aist@users.noreply.github.com> Date: Sat, 9 Nov 2024 16:35:49 +0900 Subject: [PATCH] convergence of functions wrt deleted nbhs (#1385) * convergence of functions wrt deleted nbhs --------- Co-authored-by: IshiguroYoshihiro --- CHANGELOG_UNRELEASED.md | 2 ++ theories/realfun.v | 14 ++++++++++++++ 2 files changed, 16 insertions(+) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index b5153bd4d..92c340e0d 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -69,6 +69,8 @@ - in `measure.v`: + lemma `countable_measurable` +- in `realfun.v`: + + lemma `cvgr_dnbhsP` ### Changed diff --git a/theories/realfun.v b/theories/realfun.v index bb902bfa2..ebf570f54 100644 --- a/theories/realfun.v +++ b/theories/realfun.v @@ -207,6 +207,20 @@ apply: pfl. by split; [move=> k; rewrite ltrNl//|apply/cvgNP => /=; rewrite opprK]. Qed. +Lemma cvgr_dnbhsP (f : R -> R) (p l : R) : + f x @[x --> p^'] --> l <-> + (forall u : R^nat, (forall n, u n != p) /\ (u n @[n --> \oo] --> p) -> + f (u n) @[n --> \oo] --> l). +Proof. +split=> [/cvgrPdist_le fpl u [up /cvgrPdist_lt put]|pfl]. + apply/cvgrPdist_le => e /fpl [r /=] /put[n _ {}put] {}fpl. + near=> t; apply: fpl => //=; apply: put. + by near: t; exact: nbhs_infty_ge. +apply: cvg_at_right_left_dnbhs. +- by apply/cvg_at_rightP => u [pu ?]; apply: pfl; split => // n; rewrite gt_eqF. +- by apply/cvg_at_leftP => u [pu ?]; apply: pfl; split => // n; rewrite lt_eqF. +Unshelve. all: end_near. Qed. + End cvgr_fun_cvg_seq. Section cvge_fun_cvg_seq.