proposition: Lemma MeasureIntersectSeqDecr : forall {IS : IntegrationSpace} (An : nat -> X (ElemFunc IS) -> Prop) (AnInt : forall n:nat, IntegrableSet (An n)), (forall (n : nat) (x : X (ElemFunc IS)), An (S n) x -> An n x) -> forall n : nat, MeasureSet (IntegrableSetIntersectIterate An AnInt n) == MeasureSet (AnInt n).
proof: Proof. intros IS An AnInt H. assert (forall (n : nat) (x : X (ElemFunc IS)) (xIntersect : Domain (@CharacFunc (RealT (ElemFunc IS)) _ (IntersectIterate An n)) x) (xLast : Domain (CharacFunc (An n)) x), partialApply _ _ xIntersect = partialApply _ _ xLast). { induction n. - intros. simpl. destruct xIntersect, xLast. reflexivity. contradiction. contradiction. reflexivity. - intros. specialize (H n). destruct n. + clear IHn. simpl. destruct xIntersect, xLast. reflexivity. destruct i. contradiction. 2: reflexivity. exfalso. apply n. split. apply H, a. exact a. + simpl. simpl in IHn, xIntersect. destruct xIntersect. destruct a. destruct xLast. reflexivity. contradiction. destruct xLast. 2: reflexivity. assert (~ (IntersectIterate An n x /\ An (S n) x)). intro abs. apply n0. split; assumption. specialize (H x a). specialize (IHn x (right H0) (left H)). exact IHn. } intros. apply IntegralExtensional. intros. rewrite (H0 _ _ _ xdg). reflexivity. Qed.
imports: Logic.ConstructiveEpsilon QArith ConstructiveReals ConstructiveAbs ConstructiveMinMax ConstructiveSum ConstructivePower ConstructiveLimits ConstructiveDiagonal ConstructivePartialFunctions CMTbase CMTIntegrableFunctions CMTFullSets CMTPositivity