proposition: Lemma ae_eq_subset mu A B f g : B `<=` A -> ae_eq mu A f g -> ae_eq mu B f g.
proof: Proof. move=> BA [N [mN N0 fg]]; exists N; split => //. by apply: subset_trans fg; apply: subsetC => z /= /[swap] /BA ? ->. 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)