proposition: Lemma ae_eq_comp (j : \bar R -> \bar R) f g : ae_eq f g -> ae_eq (j \o f) (j \o g).
proof: Proof. by apply: filterS => x /[apply] /= ->. 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)