proposition: Lemma MeasureExtensional : forall {IS : IntegrationSpace} (A B : (X (ElemFunc IS)) -> Prop) (Aint : IntegrableSet A) (Bint : IntegrableSet B), (forall x:X (ElemFunc IS), { A x } + { ~A x } -> { B x } + { ~B x } -> (A x <-> B x)) -> MeasureSet Aint == MeasureSet Bint.
proof: Proof. intros. apply IntegralExtensional. intros. simpl. destruct xdf, xdg. reflexivity. 3: reflexivity. exfalso. rewrite H in a. contradiction. left. exact a. right. exact n. exfalso. rewrite <- H in b. contradiction. right. exact n. left. exact b. Qed.
imports: Logic.ConstructiveEpsilon QArith ConstructiveReals ConstructiveAbs ConstructiveMinMax ConstructiveSum ConstructivePower ConstructiveLimits ConstructiveDiagonal ConstructivePartialFunctions CMTbase CMTIntegrableFunctions CMTFullSets CMTPositivity