proposition: Lemma measurable_fun_if (g h : T1 -> T2) D (mD : measurable D) (f : T1 -> bool) (mf : measurable_fun D f) : measurable_fun (D `&` (f @^-1` [set true])) g -> measurable_fun (D `&` (f @^-1` [set false])) h -> measurable_fun D (fun t => if f t then g t else h t).
proof: Proof. move=> mx my /= _ B mB; rewrite (_ : _ @^-1` B = ((f @^-1` [set true]) `&` (g @^-1` B)) `|` ((f @^-1` [set false]) `&` (h @^-1` B))). rewrite setIUr; apply: measurableU. - by rewrite setIA; apply: mx => //; exact: mf. - by rewrite setIA; apply: my => //; exact: mf. apply/seteqP; split=> [t /=| t /= [] [] ->//]. by case: ifPn => ft; [left|right]. 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)