equal
deleted
inserted
replaced
513 hence "(\<Inter>i\<in>{1..}. Z i) \<noteq> {}" by auto |
513 hence "(\<Inter>i\<in>{1..}. Z i) \<noteq> {}" by auto |
514 hence "(\<Inter>i. Z i) \<noteq> {}" using Z INT_decseq_offset[OF `decseq Z`] by simp |
514 hence "(\<Inter>i. Z i) \<noteq> {}" using Z INT_decseq_offset[OF `decseq Z`] by simp |
515 thus False using Z by simp |
515 thus False using Z by simp |
516 qed |
516 qed |
517 ultimately show "(\<lambda>i. \<mu>G (Z i)) ----> 0" |
517 ultimately show "(\<lambda>i. \<mu>G (Z i)) ----> 0" |
518 using LIMSEQ_ereal_INFI[of "\<lambda>i. \<mu>G (Z i)"] by simp |
518 using LIMSEQ_INF[of "\<lambda>i. \<mu>G (Z i)"] by simp |
519 qed |
519 qed |
520 then guess \<mu> .. note \<mu> = this |
520 then guess \<mu> .. note \<mu> = this |
521 def f \<equiv> "finmap_of J B" |
521 def f \<equiv> "finmap_of J B" |
522 show "emeasure (lim\<^isub>B I P) (emb I J (Pi\<^isub>E J B)) = emeasure (lim\<^isub>B J P) (Pi\<^isub>E J B)" |
522 show "emeasure (lim\<^isub>B I P) (emb I J (Pi\<^isub>E J B)) = emeasure (lim\<^isub>B J P) (Pi\<^isub>E J B)" |
523 proof (subst emeasure_extend_measure_Pair[OF limP_def, of I "\<lambda>_. borel" \<mu>]) |
523 proof (subst emeasure_extend_measure_Pair[OF limP_def, of I "\<lambda>_. borel" \<mu>]) |