proposition: Lemma kernel_measurable_eq_cst d d' (T : measurableType d) (T' : measurableType d') (R : realType) (f : R.-ker T ~> T') k : measurable [set t | f t [set: T'] == k].
proof: Proof. rewrite [X in measurable X](_ : _ = (f ^~ setT) @^-1` [set k]); last first. by apply/seteqP; split => t/= /eqP. have /(_ measurableT [set k]) := measurable_kernel f setT measurableT. by rewrite setTI; exact. 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