From bf79201ad4547e58937f70585dd3993ed8bf24f9 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Sun, 24 Nov 2024 23:11:14 +0900 Subject: [PATCH] fix technical lemma --- theories/measure.v | 12 +++++++----- 1 file changed, 7 insertions(+), 5 deletions(-) diff --git a/theories/measure.v b/theories/measure.v index 6cfd34f05..78b70f5e5 100644 --- a/theories/measure.v +++ b/theories/measure.v @@ -866,11 +866,12 @@ case=> ? DC DU; split => [| |? ? ?]; last exact: DU. - by move=> A GA; rewrite -setTD; apply: DC. Qed. -Lemma dynkin_setI_bigsetI G (F : (set T)^nat) : dynkin G -> setI_closed G -> - (forall n, G (F n)) -> forall n, G (\big[setI/setT]_(i < n) F i). +Lemma setT_setI_bigsetI (I0 : choiceType) (J : seq I0) G (F : I0 -> set T) : + G [set: T] -> setI_closed G -> (forall i, i \in J -> G (F i)) -> + G (\big[setI/setT]_(i <- J) F i). Proof. -move=> dG GI GF; elim => [|n ih]; last by rewrite big_ord_recr /=; apply: GI. -by rewrite big_ord0; exact: (dynkinT dG). +move=> GT GI; rewrite big_seq; elim/big_rec : _ => //. +by move=> i A iJ ih GF; apply: GI => //; [exact: GF|exact: ih]. Qed. Lemma dynkin_setI_sigma_algebra G : dynkin G -> setI_closed G -> @@ -882,7 +883,8 @@ move=> dG GI; split => [|//|F DF]. - rewrite seqDU_bigcup_eq; apply/(dynkinU dG) => //. move=> n; rewrite /seqDU setDE; apply GI => //. rewrite -bigcup_mkord setC_bigcup bigcap_mkord. - by apply: (@dynkin_setI_bigsetI _ (fun x => ~` F x)) => // ?; exact/(dynkinC dG). + apply: setT_setI_bigsetI => //=; first by case: dG. + by move=> i _; exact/(dynkinC dG). Qed. Lemma setI_closed_g_dynkin_g_sigma_algebra G :