proposition: Lemma eq_sfkernel d d' (T : measurableType d) (T' : measurableType d') (R : realType) (k1 k2 : R.-sfker T ~> T') : (forall x U, k1 x U = k2 x U) -> k1 = k2.
proof: Proof. move: k1 k2 => [m1 [[?] [?]]] [m2 [[?] [?]]] /= k12. have ? : m1 = m2. by apply/funext => t; apply/eq_measure; apply/funext => U; rewrite k12. by subst m1; f_equal; f_equal; f_equal; apply/Prop_irrelevance. 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