proposition: Lemma measurable_fun_ifT (g h : T1 -> T2) (f : T1 -> bool) (mf : measurable_fun setT f) : measurable_fun setT g -> measurable_fun setT h -> measurable_fun setT (fun t => if f t then g t else h t).
proof: Proof. by move=> mx my; apply: measurable_fun_if => //; [exact: measurable_funS mx|exact: measurable_funS my]. 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)