proposition: Lemma preimage_classes_comp : preimage_classes (f1 \o g) (f2 \o g) = preimage_class setT g (preimage_classes f1 f2).
proof: Proof. rewrite {1}/preimage_classes -sigma_algebra_preimage_classE; congr (<<s _ >>). rewrite predeqE => C; split. - move=> [[A mA <-{C}]|[A mA <-{C}]]. + by exists (f1 @^-1` A) => //; left; exists A => //; rewrite setTI. + by exists (f2 @^-1` A) => //; right; exists A => //; rewrite setTI. - move=> [A [[B mB <-{A} <-{C}]|[B mB <-{A} <-{C}]]]. + by left; rewrite !setTI; exists B => //; rewrite setTI. + by right; rewrite !setTI; exists B => //; rewrite setTI. Qed.
imports: mathcomp(all_ssreflect all_algebra finmap) mathcomp(mathcomp_extra boolp classical_sets functions) mathcomp(cardinality fsbigop ) reals ereal signed topology normedtype sequences esum numfun HB(structures)