minor generalization and renaming

CHANGELOG_UNRELEASED.md

@@ -4,8 +4,6 @@
 
 ### Added
 
-### Changed
-
 - in `mathcomp_extra.v`:
   + lemmas `prodr_ile1`, `nat_int`
 
@@ -27,7 +25,10 @@
   + lemma `pi_irrationnal`
 
 - in `numfun.v`
-	+ lemmas `funeposE`, `funenegE`, `funepos_comp`, `funeneg_comp`
+  + lemmas `funeposE`, `funenegE`, `funepos_comp`, `funeneg_comp`
+
+- in `classical_sets.v`:
+  + lemmas `xsectionE`, `ysectionE`
 
 ### Changed
 
@@ -38,10 +39,23 @@
   + put the notation ``` ^`() ``` and ``` ^`( _ ) ``` in scope `classical_set_scope`
 
 - in `numfun.v`
-	+ lock `funepos`, `funeneg`
-
+  + lock `funepos`, `funeneg`
+
+- moved from `lebesgue_integral.v` to `measure.v` and generalized
+  + lemmas `measurable_xsection`, `measurable_ysection`
+
 ### Renamed
 
+- in `measure.v`
+  + `preimage_class` -> `preimage_set_system`
+  + `image_class` -> `image_set_system`
+  + `preimage_classes` -> `g_sigma_preimageU`
+  + `preimage_class_measurable_fun` -> `preimage_set_system_measurable_fun`
+  + `sigma_algebra_preimage_class` -> `sigma_algebra_preimage`
+  + `sigma_algebra_image_class` -> `sigma_algebra_image`
+  + `sigma_algebra_preimage_classE` -> `g_sigma_preimageE`
+  + `preimage_classes_comp` -> `g_sigma_preimageU_comp`
+
 ### Generalized
 
 ### Deprecated

classical/classical_sets.v

@@ -3263,11 +3263,17 @@ Proof. by apply/idP/idP => [|]; [rewrite inE|rewrite /ysection !inE /= inE]. Qed
 Lemma ysectionP x y A : ysection A y x <-> A (x, y).
 Proof. by rewrite /ysection/= inE. Qed.
 
+Lemma xsectionE A x : xsection A x = (fun y => (x, y)) @^-1` A.
+Proof. by apply/seteqP; split => [y|y] /xsectionP. Qed.
+
+Lemma ysectionE A y : ysection A y = (fun x => (x, y)) @^-1` A.
+Proof. by apply/seteqP; split => [x|x] /ysectionP. Qed.
+
 Lemma xsection0 x : xsection set0 x = set0.
-Proof. by rewrite predeqE /xsection => y; split => //=; rewrite inE. Qed.
+Proof. by rewrite xsectionE preimage_set0. Qed.
 
 Lemma ysection0 y : ysection set0 y = set0.
-Proof. by rewrite predeqE /ysection => x; split => //=; rewrite inE. Qed.
+Proof. by rewrite ysectionE preimage_set0. Qed.
 
 Lemma in_xsectionX X1 X2 x : x \in X1 -> xsection (X1 `*` X2) x = X2.
 Proof.

theories/lebesgue_integral.v

@@ -4799,24 +4799,6 @@ End integral_ae_eq.
 
 (** Product measure *)
 
-Section measurable_section.
-Context d1 d2 (T1 : measurableType d1) (T2 : measurableType d2) (R : realType).
-Implicit Types (A : set (T1 * T2)).
-
-Lemma measurable_xsection A x : measurable A -> measurable (xsection A x).
-Proof.
-move=> mA; rewrite (xsection_indic R) -(setTI (_ @^-1` _)).
-exact: measurableT_comp.
-Qed.
-
-Lemma measurable_ysection A y : measurable A -> measurable (ysection A y).
-Proof.
-move=> mA; rewrite (ysection_indic R) -(setTI (_ @^-1` _)).
-exact: measurableT_comp.
-Qed.
-
-End measurable_section.
-
 Section ndseq_closed_B.
 Context d1 d2 (T1 : measurableType d1) (T2 : measurableType d2) (R : realType).
 Implicit Types A : set (T1 * T2).