fixes #1790 (#1799)

Author: affeldt-aist

CHANGELOG_UNRELEASED.md

@@ -196,6 +196,9 @@
 - in `charge.v`:
   + lemma `dominates_charge_variation` (use `charge_null_dominatesP` instead)
 
+- in `set_interval.v`:
+  + lemma `interval_set1` (use `set_itv1` instead)
+
 ### Infrastructure
 
 ### Misc

classical/set_interval.v

@@ -1,4 +1,4 @@
-(* mathcomp analysis (c) 2017 Inria and AIST. License: CeCILL-C.              *)
+(* mathcomp analysis (c) 2025 Inria and AIST. License: CeCILL-C.              *)
 From HB Require Import structures.
 From mathcomp Require Import all_ssreflect ssralg ssrnum interval.
 From mathcomp Require Import mathcomp_extra unstable boolp classical_sets.
@@ -120,12 +120,6 @@ move: b be zb => [[|]/= b|[|]//]; rewrite bnd_simp => be.
 by move=> /le_lt_trans; exact.
 Qed.
 
-Lemma interval_set1 x : `[x, x]%classic = [set x] :> set T.
-Proof.
-apply/seteqP; split => [y/=|y <-]; last by rewrite /= in_itv/= lexx.
-by rewrite in_itv/= => /andP[yx xy]; apply/eqP; rewrite eq_le yx xy.
-Qed.
-
 Lemma set_itvoo x y : `]x, y[%classic = [set z | (x < z < y)%O].
 Proof. by []. Qed.
 
@@ -230,6 +224,8 @@ Notation set_itv_infty_c := set_itvNyc (only parsing).
 Notation set_itv_pinfty_bnd := set_itv_ybnd (only parsing).
 #[deprecated(since="mathcomp-analysis 1.10.0", note="renamed to `set_itv_bndNy`")]
 Notation set_itv_bnd_ninfty := set_itv_bndNy (only parsing).
+#[deprecated(since="mathcomp-analysis 1.15.0", note="use `set_itv1` instead")]
+Notation interval_set1 := set_itv1 (only parsing).
 
 Section set_itv_orderType.
 Variables (d : Order.disp_t) (T : orderType d).

theories/ftc.v

@@ -463,7 +463,7 @@ rewrite le_eqVlt => /predU1P[<- _|ab intf].
 apply/(continuous_within_itvP _ ab); split; first last.
   exact: parameterized_integral_cvg_at_left.
   apply/cvg_at_right_filter.
-  rewrite {2}/int /parameterized_integral interval_set1 Rintegral_set1.
+  rewrite {2}/int /parameterized_integral set_itv1 Rintegral_set1.
   exact: (parameterized_integral_cvg_left ab).
 pose fab := f \_ `[a, b].
 have /= int_normr_cont : forall e : R, 0 < e ->
@@ -630,10 +630,10 @@ have Ga : G x @[x --> a^'+] --> G a.
    have := parameterized_integral_cvg_left ab iabfab.
    rewrite (_ : 0 = G a)%R.
      by move=> /left_right_continuousP[].
-   by rewrite /G interval_set1 Rintegral_set1.
+   by rewrite /G set_itv1 Rintegral_set1.
 have Gb : G x @[x --> b^'-] --> G b.
   exact: (parameterized_integral_cvg_at_left ab iabfab).
-have Ga0 : G a = 0%R by rewrite /G interval_set1// Rintegral_set1.
+have Ga0 : G a = 0%R by rewrite /G set_itv1// Rintegral_set1.
 have cE : c = F a.
   apply/eqP; rewrite -(opprK c) eq_sym -addr_eq0 addrC.
   by have := cvg_unique _ GacFa Ga; rewrite Ga0 => ->.