proposition: Lemma measure_le0 d (T : semiRingOfSetsType d) (R : realFieldType) (mu : {content set T -> \bar R}) (A : set T) : (mu A <= 0)%E = (mu A == 0)%E.
proof: Proof. by case: ltgtP (measure_ge0 mu A). 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)