src/HOL/Probability/Infinite_Product_Measure.thy
changeset 42950 6e5c2a3c69da
parent 42866 b0746bd57a41
child 43679 052eaf7509cf
     1.1 --- a/src/HOL/Probability/Infinite_Product_Measure.thy	Mon May 23 10:58:21 2011 +0200
     1.2 +++ b/src/HOL/Probability/Infinite_Product_Measure.thy	Mon May 23 19:21:05 2011 +0200
     1.3 @@ -223,11 +223,6 @@
     1.4      done
     1.5  qed
     1.6  
     1.7 -lemma (in prob_space) measure_le_1: "X \<in> sets M \<Longrightarrow> \<mu> X \<le> 1"
     1.8 -  unfolding measure_space_1[symmetric]
     1.9 -  using sets_into_space
    1.10 -  by (intro measure_mono) auto
    1.11 -
    1.12  definition (in product_prob_space)
    1.13    "\<mu>G A =
    1.14      (THE x. \<forall>J. J \<noteq> {} \<longrightarrow> finite J \<longrightarrow> J \<subseteq> I \<longrightarrow> (\<forall>X\<in>sets (Pi\<^isub>M J M). A = emb I J X \<longrightarrow> x = measure (Pi\<^isub>M J M) X))"