Fixes 1998 (#1999)

* fixes #1998

* partly address issue 1968

* partly address issue 1967

* fixes #1957

Author: affeldt-aist

CHANGELOG_UNRELEASED.md

@@ -303,6 +303,10 @@
 - in `measurable_structure.v`:
   + lemmas `measurable_prod_g_measurableType`, `measurable_prod_g_measurableTypeR`
 
+- file `measurable_structure.v`:
+  + notations `preimage_class`, `image_class`, `sigma_algebra_preimage_class`,
+    `sigma_algebra_image_class`, `sigma_algebra_preimage_classE` (deprecated since 1.9.0)
+
 ### Infrastructure
 
 ### Misc

classical/classical_sets.v

@@ -108,6 +108,8 @@ From mathcomp Require Import mathcomp_extra boolp wochoice.
 (*               rectangle X Y := [set U `*` V | U in X & V in Y]             *)
 (*   preimage_set_system D f G == set system of the preimages by f of sets    *)
 (*                                in G                                        *)
+(*      image_set_system D f G == set system of the sets with a preimage      *)
+(*                                by f in G                                   *)
 (*               cross f g X Y := preimage_set_system setT f X                *)
 (*                                `|` preimage_set_system setT g Y            *)
 (*                     X `x` Y := cross fst snd X Y                           *)
@@ -1717,6 +1719,10 @@ Lemma preimage_set_systemS {T1 T2} (A B : set_system T2) (f : T1 -> T2) :
   preimage_set_system [set: _] f A `<=` preimage_set_system [set: _] f B.
 Proof. by move=> AB _ [C ? <-]; exists C => //; exact: AB. Qed.
 
+Definition image_set_system (aT rT : Type) (D : set aT) (f : aT -> rT)
+    (G : set (set aT)) : set (set rT) :=
+  [set B : set rT | G (D `&` f @^-1` B)].
+
 Section cross.
 Context {T T1 T2 : Type}.
 Implicit Types (X : set_system T1) (Y : set_system T2).

classical/filter.v

@@ -1,6 +1,6 @@
 (* mathcomp analysis (c) 2026 Inria and AIST. License: CeCILL-C.              *)
 From HB Require Import structures.
-From mathcomp Require Import all_ssreflect_compat all_algebra finmap.
+From mathcomp Require Import all_ssreflect_compat algebra finmap.
 From mathcomp Require Import boolp classical_sets functions wochoice.
 From mathcomp Require Import cardinality mathcomp_extra fsbigop set_interval.
 

classical/functions.v

@@ -2656,7 +2656,7 @@ Let mulrC : commutative (@GRing.mul (T -> M)).
 Proof. by move=> f g; rewrite funeqE => x; rewrite /GRing.mul/= mulrC. Qed.
 
 HB.instance Definition _ :=
-  GRing.PzRing_hasCommutativeMul.Build (T -> M) mulrC.
+  GRing.SemiRing_hasCommutativeMul.Build (T -> M) mulrC.
 
 End fct_comPzRingType.
 

classical/mathcomp_extra.v

@@ -1,6 +1,6 @@
 (* mathcomp analysis (c) 2026 Inria and AIST. License: CeCILL-C.              *)
 From HB Require Import structures.
-From mathcomp Require Import all_ssreflect_compat finmap all_algebra.
+From mathcomp Require Import all_ssreflect_compat finmap algebra.
 
 (**md**************************************************************************)
 (* # MathComp extra                                                           *)

experimental_reals/discrete.v

@@ -6,7 +6,7 @@
 (* -------------------------------------------------------------------- *)
 From Corelib Require Setoid.
 From HB Require Import structures.
-From mathcomp Require Import all_ssreflect_compat all_algebra.
+From mathcomp Require Import all_ssreflect_compat algebra.
 From mathcomp.classical Require Import boolp.
 From mathcomp Require Import xfinmap reals.
 

experimental_reals/distr.v

@@ -4,7 +4,7 @@
 (* Copyright (c) - 2016--2018 - Polytechnique                           *)
 
 (* -------------------------------------------------------------------- *)
-From mathcomp Require Import all_ssreflect_compat all_algebra.
+From mathcomp Require Import all_ssreflect_compat algebra.
 From mathcomp.classical Require Import boolp classical_sets mathcomp_extra.
 From mathcomp Require Import xfinmap constructive_ereal reals discrete.
 From mathcomp Require Import realseq realsum.

experimental_reals/realseq.v

@@ -4,7 +4,7 @@
 (* Copyright (c) - 2016--2018 - Polytechnique                           *)
 
 (* -------------------------------------------------------------------- *)
-From mathcomp Require Import all_ssreflect_compat all_algebra.
+From mathcomp Require Import all_ssreflect_compat algebra.
 From mathcomp Require Import bigenough.
 From mathcomp.classical Require Import boolp classical_sets functions.
 From mathcomp.classical Require Import mathcomp_extra.

experimental_reals/realsum.v

@@ -3,7 +3,7 @@
 (* Copyright (c) - 2015--2018 - Inria                                   *)
 (* Copyright (c) - 2016--2018 - Polytechnique                           *)
 (* -------------------------------------------------------------------- *)
-From mathcomp Require Import all_ssreflect_compat all_algebra.
+From mathcomp Require Import all_ssreflect_compat algebra.
 #[warning="-warn-library-file-internal-analysis"]
 From mathcomp Require Import unstable.
 From mathcomp.classical Require Import boolp.

experimental_reals/xfinmap.v

@@ -4,7 +4,7 @@
 (* Copyright (c) - 2016--2018 - Polytechnique                           *)
 
 (* -------------------------------------------------------------------- *)
-From mathcomp Require Import all_ssreflect_compat all_algebra.
+From mathcomp Require Import all_ssreflect_compat algebra.
 From mathcomp Require Export finmap.
 
 Unset SsrOldRewriteGoalsOrder.  (* remove the line when requiring MathComp >= 2.6 *)