proposition: Lemma eq_measurable_fun D (f g : T1 -> T2) : {in D, f =1 g} -> measurable_fun D f -> measurable_fun D g.
proof: Proof. by move=> fg mf mD A mA; rewrite [X in measurable X](_ : _ = D `&` f @^-1` A); [exact: mf|exact/esym/eq_preimage]. 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)