minor gen and rm dup

CHANGELOG_UNRELEASED.md

@@ -110,6 +110,9 @@
   + lemmas `derive1_comp`, `is_derive1_comp` (`realFieldType` -> `numFieldType`)
   + lemmas `derive_shift`, `is_derive_shift` (function codomain)
 
+- in `pseudometric_normed_Zmodule.v`:
+  + lemma `within_continuous_continuous`
+
 ### Deprecated
 
 ### Removed

theories/ftc.v

@@ -1013,24 +1013,6 @@ Unshelve. all: end_near. Qed.
 
 End integration_by_substitution_preliminaries.
 
-(* PR in progress *)
-Lemma cvgNy_compNP {T : topologicalType} {R : numFieldType} (f : R -> T)
-    (l : set_system T) :
-  f x @[x --> -oo] --> l <-> (f \o -%R) x @[x --> +oo] --> l.
-Proof.
-have f_opp : f =1 (fun x => (f \o -%R) (- x)) by move=> x; rewrite /comp opprK.
-by rewrite (eq_cvg -oo _ f_opp) [in X in X <-> _]fmap_comp ninftyN.
-Qed.
-
-(* PR in progress *)
-Lemma cvgy_compNP {T : topologicalType} {R : numFieldType} (f : R -> T)
-    (l : set_system T) :
-  f x @[x --> +oo] --> l <-> (f \o -%R) x @[x --> -oo] --> l.
-Proof.
-have f_opp : f =1 (fun x => (f \o -%R) (- x)) by move=> x; rewrite /comp opprK.
-by rewrite (eq_cvg +oo _ f_opp) [in X in X <-> _]fmap_comp ninfty.
-Qed.
-
 Section integration_by_substitution.
 Local Open Scope ereal_scope.
 Context {R : realType}.
@@ -1071,10 +1053,10 @@ pose PG x := parameterized_integral mu (F b) x G.
 have PGFbFa : derivable_oo_LRcontinuous PG (F b) (F a).
   have [/= dF rF lF] := Fab; split => /=.
   - move=> x xFbFa /=.
-    have xFa : (x < F a)%R. by move: xFbFa; rewrite in_itv/= => /andP[].
+    have xFa : (x < F a)%R by move: xFbFa; rewrite in_itv/= => /andP[].
     apply: (continuous_FTC1 xFa intG _ _).1 => /=.
       by move: xFbFa; rewrite lte_fin in_itv/= => /andP[].
-    exact: (within_continuous_continuous _ _ xFbFa).
+    exact: (within_continuous_continuous (ltW _) _ xFbFa).
   - have := parameterized_integral_continuous (ltW FbFa) intG.
     by move=> /(continuous_within_itvP _ FbFa)[].
   - exact: parameterized_integral_cvg_at_left.
@@ -1090,7 +1072,7 @@ rewrite (@continuous_FTC2 _ _ PG _ _ FbFa cG).
   have xFa : (x < F a)%R by move: xFbFa; rewrite in_itv/= => /andP[].
   apply: (continuous_FTC1 xFa _ _ _).2 => //=.
     by move: xFbFa; rewrite lte_fin in_itv/= => /andP[].
-  exact: (within_continuous_continuous _ _ xFbFa).
+  exact: (within_continuous_continuous (ltW _) _ xFbFa).
 set f  := fun x => if x == a then r else if x == b then l else F^`() x.
 have fE : {in `]a, b[, F^`() =1 f}.
   by move=> x; rewrite in_itv/= => /andP[ax xb]; rewrite /f gt_eqF// lt_eqF.
@@ -1108,7 +1090,7 @@ have DPGFE : {in `]a, b[, (- (PG \o F))%R^`() =1 ((G \o F) * (- f))%R}.
   have /[dup]FxFbFa : F x \in `]F b, F a[ by exact: decreasing_image_oo.
   rewrite in_itv/= => /andP[FbFx FxFa].
   apply: (continuous_FTC1 FxFa intG FbFx _).2 => //=.
-  exact: (within_continuous_continuous _ _ FxFbFa).
+  exact: (within_continuous_continuous (ltW _) _ FxFbFa).
 rewrite -[LHS]oppeK oppeB// addrC.
 under eq_integral do rewrite mulrN EFinN.
 rewrite oppeD//= -(continuous_FTC2 ab _ _ DPGFE).

theories/normedtype_theory/pseudometric_normed_Zmodule.v

@@ -1089,10 +1089,12 @@ Qed.
 End continuous_within_itvP.
 
 Lemma within_continuous_continuous {R : realFieldType} {K : numDomainType}
-    {U : pseudoMetricNormedZmodType K} a b (f : R -> U) x : (a < b)%R ->
-  {within `[a, b], continuous f} -> x \in `]a, b[ -> {for x, continuous f}.
+    {U : pseudoMetricNormedZmodType K} a b (f : R -> U) x : (a <= b)%R ->
+  {within `[a, b], continuous f} -> x \in `]a, b[%R -> {for x, continuous f}.
 Proof.
-by move=> ab /continuous_within_itvP-/(_ ab)[+ _] /[swap] xab cf; exact.
+rewrite le_eqVlt => /predU1P[<- _|ab].
+  by rewrite in_itv/= => /andP[] /lt_trans /[apply]; rewrite ltxx.
+by move=> /continuous_within_itvP-/(_ ab)[+ _ _]; exact.
 Qed.
 
 Module Export NearNorm.