proposition: Lemma probability_setC (A : set T) : measurable A -> P (~` A) = 1 - P A.
proof: Proof. move=> mA. rewrite -(@probability_setT _ _ _ P) -(setvU A) measureU ?addeK ?setICl//. - by rewrite fin_num_measure. - exact: measurableC. 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)