proposition: Lemma MeasurableFunctionFull : forall {IS : IntegrationSpace} (f : PartialFunction (X (ElemFunc IS))), MeasurableFunction f -> almost_everywhere (Domain f).
proof: Proof. intros IS f fMes. destruct (@PositiveMeasureSubsetExists IS) as [A Aint Apos]. specialize (fMes A 1%positive Aint). exists (XmaxConst (XminConst (Xmult (CharacFunc A) f) (CR_of_Q (RealT (ElemFunc IS)) 1)) (CR_of_Q (RealT (ElemFunc IS)) (-1))). split. exact fMes. intros x xD. apply xD. Qed.
imports: QArith ConstructiveReals ConstructiveAbs ConstructiveMinMax ConstructiveSum ConstructivePower ConstructiveLimits ConstructivePartialFunctions CMTbase CMTIntegrableFunctions CMTFullSets CMTIntegrableSets CMTprofile