preimage_set_system lemmas

CHANGELOG_UNRELEASED.md

@@ -25,6 +25,10 @@
 - in `trigo.v`:
   + lemma `integral0oo_atan`
 
+- in `measure.v`:
+  + lemmas `preimage_set_system0`, `preimage_set_systemU`, `preimage_set_system_comp`
+  + lemma `preimage_set_system_id`
+
 ### Changed
 
 - file `nsatz_realtype.v` moved from `reals` to `reals-stdlib` package

theories/measure.v

@@ -1705,10 +1705,32 @@ Notation measurable_funT_comp := measurableT_comp (only parsing).
 
 Section measurability.
 
-Definition preimage_set_system (aT rT : Type) (D : set aT) (f : aT -> rT)
-    (G : set (set rT)) : set (set aT) :=
+Definition preimage_set_system {aT rT : Type} (D : set aT) (f : aT -> rT)
+    (G : set_system rT) : set (set aT) :=
   [set D `&` f @^-1` B | B in G].
 
+Lemma preimage_set_system0 {aT rT : Type} (D : set aT) (f : aT -> rT) :
+  preimage_set_system D f set0 = set0.
+Proof. exact: image_set0. Qed.
+
+Lemma preimage_set_systemU {aT rT : Type} (D : set aT) (f : aT -> rT) :
+  {morph preimage_set_system D f : x y / x `|` y >-> x `|` y}.
+Proof. exact: image_setU. Qed.
+
+Lemma preimage_set_system_comp {aT bT rT : Type} (D : set aT)
+    (f : aT -> bT) (g : bT -> rT) (F : set_system rT) :
+  preimage_set_system D (g \o f) F
+    = preimage_set_system D f (preimage_set_system setT g F).
+Proof.
+apply/seteqP; split=> [_ [B FB] <-|_ [_ [C FC <-] <-]].
+  by exists (g @^-1` B) => //; exists B => //; rewrite setTI.
+by exists C => //; rewrite setTI comp_preimage.
+Qed.
+
+Lemma preimage_set_system_id {aT : Type} (D : set aT) (F : set (set aT)) :
+  preimage_set_system D idfun F = setI D @` F.
+Proof. by []. Qed.
+
 (* f is measurable on the sigma-algebra generated by itself *)
 Lemma preimage_set_system_measurable_fun d (aT : pointedType)
     (rT : measurableType d) (D : set aT) (f : aT -> rT) :