proposition: Lemma open_measurable_subspace (D : set R) (U : set (subspace D)) : measurable D -> open U -> measurable (D `&` U).
proof: Proof. move=> mD /open_subspaceP [V [oV] VD]; rewrite setIC -VD. by apply: measurableI => //; exact: open_measurable. 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