proposition: Lemma measurable_fun_if_pair d d' (X : measurableType d) (Y : measurableType d') (x y : X -> Y) : measurable_fun setT x -> measurable_fun setT y -> measurable_fun setT (fun tb => if tb.2 then x tb.1 else y tb.1).
proof: Proof. by move=> mx my; apply: measurable_fun_ifT => //=; exact: measurableT_comp. 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)