proposition: Lemma measurable_restrict D E (f : T1 -> T2) : measurable D -> measurable E -> D `<=` E -> measurable_fun D f <-> measurable_fun E (f \_ D).
proof: Proof. move=> mD mE DE; split => mf _ /= X mX. - rewrite preimage_restrict; apply/measurableI => //. by apply/measurableU/mf => //; case: ifP => // _; apply: measurableC. - have := mf mE _ mX; rewrite preimage_restrict. case: ifP => ptX; last first. rewrite set0U => /(measurableI _ _ mD). by rewrite (setIA D) (setIidl DE) setIA setIid. rewrite setUIr setvU setTI => /(measurableI _ _ mD). by rewrite setIA (setIidl DE) setIUr setICr set0U. 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)