rename: derivable_oy_continuous_bndN -> derivable_oy_RcontinuousN

Author: t6s

CHANGELOG_UNRELEASED.md

@@ -92,7 +92,7 @@
            `derivable_Nyo_continuousW`
 
 - in `realfun.v`:
-  + lemma `derivable_oy_continuous_bndN`
+  + lemma `derivable_oy_RcontinuousN`
 
 - in `ftc.v`:
   + lemmas `integration_by_partsy_ge0_ge0`,

theories/ftc.v

@@ -1097,7 +1097,7 @@ rewrite (@integration_by_partsy_ge0_ge0 R (- F)%R G (- f)%R g a (- FGoo)).
   rewrite -EFinN opprD 2!opprK mulNr.
   by under eq_integral do rewrite mulNr EFinN.
 - by move=> ?; apply: cvgN; exact: cf.
-- exact: derivable_oy_continuous_bndN.
+- exact: derivable_oy_RcontinuousN.
 - by move=> ? ?; rewrite fctE derive1N ?Ff => [//|//|]; apply: Foy.1.
 - by [].
 - by [].
@@ -1119,7 +1119,7 @@ rewrite (@integration_by_partsy_le0_ge0 R (- F)%R G (- f)%R g a (- FGoo)).
   rewrite -EFinN opprD 2!opprK mulNr oppeK.
   by under eq_integral do rewrite mulNr EFinN.
 - by move=> ?; apply: cvgN; exact: cf.
-- exact: derivable_oy_continuous_bndN.
+- exact: derivable_oy_RcontinuousN.
 - by move=> ? ?; rewrite fctE derive1N ?Ff//; move: Foy => [+ _]; apply.
 - by [].
 - by [].

theories/realfun.v

@@ -1124,8 +1124,7 @@ Definition derivable_Nyo_Lcontinuous (f : R -> V) (x : R) :=
 Definition derivable_oy_Rcontinuous (f : R -> V) (x : R) :=
   {in `]x, +oo[, forall x, derivable f x 1} /\ f @ x^'+ --> f x.
 
-(* TODO rename to derivable_oy_Rcontinuous_bndN *)
-Lemma derivable_oy_continuous_bndN (f : R -> V) (x : R) :
+Lemma derivable_oy_RcontinuousN (f : R -> V) (x : R) :
   derivable_oy_Rcontinuous f x -> derivable_oy_Rcontinuous (- f) x.
 Proof.
 case=> /= derF Fa; split; last exact: cvgN.