proposition: Lemma kernel_measurable_fun_eq_cst d d' (T : measurableType d) (T' : measurableType d') (R : realType) (f : R.-ker T ~> T') k : measurable_fun [set: T] (fun t => f t [set: T'] == k).
proof: Proof. move=> _ /= B mB; rewrite setTI. have [/eqP->|/eqP->|/eqP->|/eqP->] := set_bool B. - exact: kernel_measurable_eq_cst. - rewrite (_ : _ @^-1` _ = [set b | f b setT != k]); last first. by apply/seteqP; split => [t /negbT//|t /negbTE]. exact: kernel_measurable_neq_cst. - by rewrite preimage_set0. - by rewrite preimage_setT. Qed.
imports: HB(structures) mathcomp(all_ssreflect ssralg ssrnum ssrint interval finmap) mathcomp(mathcomp_extra boolp classical_sets functions) mathcomp(cardinality fsbigop) reals ereal signed topology normedtype sequences esum measure numfun lebesgue_measure lebesgue_integral