proposition: Lemma lebesgue_measure_set1 (a : R) : lebesgue_measure [set a] = 0%E.
proof: Proof. suff : (lebesgue_measure (`]a - 1, a]%classic%R : set R) = lebesgue_measure (`]a - 1, a[%classic%R : set R) + lebesgue_measure [set a])%E. rewrite lebesgue_measure_itvoo_subr1 lebesgue_measure_itvoc => /eqP. rewrite wlength_itv lte_fin ltrBlDr ltrDl ltr01. rewrite [in X in X == _]/= EFinN EFinB fin_num_oppeB// addeA subee// add0e. by rewrite addeC -sube_eq ?fin_num_adde_defl// subee// => /eqP. rewrite -setUitv1// ?bnd_simp; last by rewrite ltrBlDr ltrDl. rewrite measureU //; apply/seteqP; split => // x []/=. by rewrite in_itv/= => + xa; rewrite xa ltxx andbF. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum ssrint interval) mathcomp(finmap fingroup perm rat) mathcomp(mathcomp_extra boolp classical_sets functions) mathcomp(cardinality fsbigop) reals ereal signed topology numfun normedtype HB(structures) sequences esum measure real_interval realfun exp lebesgue_stieltjes_measure