add ring_of_sets and subset_class as basis for algebra
authorhoelzl
Tue Mar 22 16:44:57 2011 +0100 (2011-03-22)
changeset 420652b98b4c2e2f1
parent 42064 f4e53c8630c0
child 42066 6db76c88907a
add ring_of_sets and subset_class as basis for algebra
src/HOL/Probability/Caratheodory.thy
src/HOL/Probability/Measure.thy
src/HOL/Probability/Sigma_Algebra.thy
     1.1 --- a/src/HOL/Probability/Caratheodory.thy	Tue Mar 22 19:04:32 2011 +0100
     1.2 +++ b/src/HOL/Probability/Caratheodory.thy	Tue Mar 22 16:44:57 2011 +0100
     1.3 @@ -217,7 +217,7 @@
     1.4  
     1.5  lemma (in algebra) lambda_system_algebra:
     1.6    "positive M f \<Longrightarrow> algebra (M\<lparr>sets := lambda_system M f\<rparr>)"
     1.7 -  apply (auto simp add: algebra_def)
     1.8 +  apply (auto simp add: algebra_iff_Un)
     1.9    apply (metis lambda_system_sets set_mp sets_into_space)
    1.10    apply (metis lambda_system_empty)
    1.11    apply (metis lambda_system_Compl)
    1.12 @@ -332,9 +332,10 @@
    1.13      by (force simp add: disjoint_family_on_def neq_iff)
    1.14    have 3: "A n \<in> lambda_system M f" using A
    1.15      by blast
    1.16 +  interpret l: algebra "M\<lparr>sets := lambda_system M f\<rparr>"
    1.17 +    using f by (rule lambda_system_algebra)
    1.18    have 4: "UNION {0..<n} A \<in> lambda_system M f"
    1.19 -    using A algebra.UNION_in_sets [OF local.lambda_system_algebra, of f, OF f]
    1.20 -    by simp
    1.21 +    using A l.UNION_in_sets by simp
    1.22    from Suc.hyps show ?case
    1.23      by (simp add: atLeastLessThanSuc lambda_system_strong_additive [OF a 2 3 4])
    1.24  qed
    1.25 @@ -352,8 +353,8 @@
    1.26      by (metis countably_subadditive_subadditive csa pos)
    1.27    have A': "range A \<subseteq> sets (M(|sets := lambda_system M f|))" using A
    1.28      by simp
    1.29 -  have alg_ls: "algebra (M(|sets := lambda_system M f|))"
    1.30 -    by (rule lambda_system_algebra) (rule pos)
    1.31 +  interpret ls: algebra "M\<lparr>sets := lambda_system M f\<rparr>"
    1.32 +    using pos by (rule lambda_system_algebra)
    1.33    have A'': "range A \<subseteq> sets M"
    1.34       by (metis A image_subset_iff lambda_system_sets)
    1.35  
    1.36 @@ -366,7 +367,7 @@
    1.37      have *: "\<And>i. 0 \<le> f (A i)" using pos A'' unfolding positive_def by auto
    1.38      have dis: "\<And>N. disjoint_family_on A {..<N}" by (intro disjoint_family_on_mono[OF _ disj]) auto
    1.39      show "(\<Sum>i. f (A i)) \<le> f (\<Union>i. A i)"
    1.40 -      using algebra.additive_sum [OF alg_ls lambda_system_positive[OF pos] lambda_system_additive _ A' dis]
    1.41 +      using ls.additive_sum [OF lambda_system_positive[OF pos] lambda_system_additive _ A' dis]
    1.42        using A''
    1.43        by (intro suminf_bound[OF _ *]) (auto intro!: increasingD[OF inc] allI countable_UN)
    1.44    qed
    1.45 @@ -401,8 +402,7 @@
    1.46              have le_fa: "f (UNION {0..<n} A \<inter> a) \<le> f a" using A''
    1.47                by (blast intro: increasingD [OF inc] A'' UNION_in_sets)
    1.48              have ls: "(\<Union>i\<in>{0..<n}. A i) \<in> lambda_system M f"
    1.49 -              using algebra.UNION_in_sets [OF lambda_system_algebra [of f, OF pos]]
    1.50 -              by (simp add: A)
    1.51 +              using ls.UNION_in_sets by (simp add: A)
    1.52              hence eq_fa: "f a = f (a \<inter> (\<Union>i\<in>{0..<n}. A i)) + f (a - (\<Union>i\<in>{0..<n}. A i))"
    1.53                by (simp add: lambda_system_eq UNION_in)
    1.54              have "f (a - (\<Union>i. A i)) \<le> f (a - (\<Union>i\<in>{0..<n}. A i))"
    1.55 @@ -441,8 +441,8 @@
    1.56      by (metis oms outer_measure_space_def)
    1.57    have alg: "algebra ?M"
    1.58      using lambda_system_algebra [of f, OF pos]
    1.59 -    by (simp add: algebra_def)
    1.60 -  then moreover
    1.61 +    by (simp add: algebra_iff_Un)
    1.62 +  then
    1.63    have "sigma_algebra ?M"
    1.64      using lambda_system_caratheodory [OF oms]
    1.65      by (simp add: sigma_algebra_disjoint_iff)
    1.66 @@ -453,7 +453,7 @@
    1.67                    countably_additive_def o_def)
    1.68    ultimately
    1.69    show ?thesis
    1.70 -    by intro_locales (auto simp add: sigma_algebra_def)
    1.71 +    by (simp add: measure_space_def)
    1.72  qed
    1.73  
    1.74  lemma (in algebra) additive_increasing:
     2.1 --- a/src/HOL/Probability/Measure.thy	Tue Mar 22 19:04:32 2011 +0100
     2.2 +++ b/src/HOL/Probability/Measure.thy	Tue Mar 22 16:44:57 2011 +0100
     2.3 @@ -18,7 +18,7 @@
     2.4  
     2.5  lemma algebra_measure_update[simp]:
     2.6    "algebra (M'\<lparr>measure := m\<rparr>) \<longleftrightarrow> algebra M'"
     2.7 -  unfolding algebra_def by simp
     2.8 +  unfolding algebra_iff_Un by simp
     2.9  
    2.10  lemma sigma_algebra_measure_update[simp]:
    2.11    "sigma_algebra (M'\<lparr>measure := m\<rparr>) \<longleftrightarrow> sigma_algebra M'"
     3.1 --- a/src/HOL/Probability/Sigma_Algebra.thy	Tue Mar 22 19:04:32 2011 +0100
     3.2 +++ b/src/HOL/Probability/Sigma_Algebra.thy	Tue Mar 22 16:44:57 2011 +0100
     3.3 @@ -28,89 +28,111 @@
     3.4    space :: "'a set"
     3.5    sets :: "'a set set"
     3.6  
     3.7 -locale algebra =
     3.8 +locale subset_class =
     3.9    fixes M :: "('a, 'b) algebra_scheme"
    3.10    assumes space_closed: "sets M \<subseteq> Pow (space M)"
    3.11 -     and  empty_sets [iff]: "{} \<in> sets M"
    3.12 -     and  compl_sets [intro]: "!!a. a \<in> sets M \<Longrightarrow> space M - a \<in> sets M"
    3.13 -     and  Un [intro]: "!!a b. a \<in> sets M \<Longrightarrow> b \<in> sets M \<Longrightarrow> a \<union> b \<in> sets M"
    3.14  
    3.15 -lemma (in algebra) top [iff]: "space M \<in> sets M"
    3.16 -  by (metis Diff_empty compl_sets empty_sets)
    3.17 -
    3.18 -lemma (in algebra) sets_into_space: "x \<in> sets M \<Longrightarrow> x \<subseteq> space M"
    3.19 +lemma (in subset_class) sets_into_space: "x \<in> sets M \<Longrightarrow> x \<subseteq> space M"
    3.20    by (metis PowD contra_subsetD space_closed)
    3.21  
    3.22 -lemma (in algebra) Int [intro]:
    3.23 +locale ring_of_sets = subset_class +
    3.24 +  assumes empty_sets [iff]: "{} \<in> sets M"
    3.25 +     and  Diff [intro]: "\<And>a b. a \<in> sets M \<Longrightarrow> b \<in> sets M \<Longrightarrow> a - b \<in> sets M"
    3.26 +     and  Un [intro]: "\<And>a b. a \<in> sets M \<Longrightarrow> b \<in> sets M \<Longrightarrow> a \<union> b \<in> sets M"
    3.27 +
    3.28 +lemma (in ring_of_sets) Int [intro]:
    3.29    assumes a: "a \<in> sets M" and b: "b \<in> sets M" shows "a \<inter> b \<in> sets M"
    3.30  proof -
    3.31 -  have "((space M - a) \<union> (space M - b)) \<in> sets M"
    3.32 -    by (metis a b compl_sets Un)
    3.33 -  moreover
    3.34 -  have "a \<inter> b = space M - ((space M - a) \<union> (space M - b))"
    3.35 -    using space_closed a b
    3.36 -    by blast
    3.37 -  ultimately show ?thesis
    3.38 -    by (metis compl_sets)
    3.39 +  have "a \<inter> b = a - (a - b)"
    3.40 +    by auto
    3.41 +  then show "a \<inter> b \<in> sets M"
    3.42 +    using a b by auto
    3.43  qed
    3.44  
    3.45 -lemma (in algebra) Diff [intro]:
    3.46 -  assumes a: "a \<in> sets M" and b: "b \<in> sets M" shows "a - b \<in> sets M"
    3.47 -proof -
    3.48 -  have "(a \<inter> (space M - b)) \<in> sets M"
    3.49 -    by (metis a b compl_sets Int)
    3.50 -  moreover
    3.51 -  have "a - b = (a \<inter> (space M - b))"
    3.52 -    by (metis Int_Diff Int_absorb1 Int_commute a sets_into_space)
    3.53 -  ultimately show ?thesis
    3.54 -    by metis
    3.55 -qed
    3.56 -
    3.57 -lemma (in algebra) finite_union [intro]:
    3.58 +lemma (in ring_of_sets) finite_Union [intro]:
    3.59    "finite X \<Longrightarrow> X \<subseteq> sets M \<Longrightarrow> Union X \<in> sets M"
    3.60    by (induct set: finite) (auto simp add: Un)
    3.61  
    3.62 -lemma (in algebra) finite_UN[intro]:
    3.63 +lemma (in ring_of_sets) finite_UN[intro]:
    3.64    assumes "finite I" and "\<And>i. i \<in> I \<Longrightarrow> A i \<in> sets M"
    3.65    shows "(\<Union>i\<in>I. A i) \<in> sets M"
    3.66    using assms by induct auto
    3.67  
    3.68 -lemma (in algebra) finite_INT[intro]:
    3.69 +lemma (in ring_of_sets) finite_INT[intro]:
    3.70    assumes "finite I" "I \<noteq> {}" "\<And>i. i \<in> I \<Longrightarrow> A i \<in> sets M"
    3.71    shows "(\<Inter>i\<in>I. A i) \<in> sets M"
    3.72    using assms by (induct rule: finite_ne_induct) auto
    3.73  
    3.74 -lemma algebra_iff_Int:
    3.75 -     "algebra M \<longleftrightarrow>
    3.76 -       sets M \<subseteq> Pow (space M) & {} \<in> sets M &
    3.77 -       (\<forall>a \<in> sets M. space M - a \<in> sets M) &
    3.78 -       (\<forall>a \<in> sets M. \<forall> b \<in> sets M. a \<inter> b \<in> sets M)"
    3.79 -proof (auto simp add: algebra.Int, auto simp add: algebra_def)
    3.80 -  fix a b
    3.81 -  assume ab: "sets M \<subseteq> Pow (space M)"
    3.82 -             "\<forall>a\<in>sets M. space M - a \<in> sets M"
    3.83 -             "\<forall>a\<in>sets M. \<forall>b\<in>sets M. a \<inter> b \<in> sets M"
    3.84 -             "a \<in> sets M" "b \<in> sets M"
    3.85 -  hence "a \<union> b = space M - ((space M - a) \<inter> (space M - b))"
    3.86 -    by blast
    3.87 -  also have "... \<in> sets M"
    3.88 -    by (metis ab)
    3.89 -  finally show "a \<union> b \<in> sets M" .
    3.90 -qed
    3.91 -
    3.92 -lemma (in algebra) insert_in_sets:
    3.93 +lemma (in ring_of_sets) insert_in_sets:
    3.94    assumes "{x} \<in> sets M" "A \<in> sets M" shows "insert x A \<in> sets M"
    3.95  proof -
    3.96    have "{x} \<union> A \<in> sets M" using assms by (rule Un)
    3.97    thus ?thesis by auto
    3.98  qed
    3.99  
   3.100 -lemma (in algebra) Int_space_eq1 [simp]: "x \<in> sets M \<Longrightarrow> space M \<inter> x = x"
   3.101 +lemma (in ring_of_sets) Int_space_eq1 [simp]: "x \<in> sets M \<Longrightarrow> space M \<inter> x = x"
   3.102    by (metis Int_absorb1 sets_into_space)
   3.103  
   3.104 -lemma (in algebra) Int_space_eq2 [simp]: "x \<in> sets M \<Longrightarrow> x \<inter> space M = x"
   3.105 +lemma (in ring_of_sets) Int_space_eq2 [simp]: "x \<in> sets M \<Longrightarrow> x \<inter> space M = x"
   3.106    by (metis Int_absorb2 sets_into_space)
   3.107  
   3.108 +locale algebra = ring_of_sets +
   3.109 +  assumes top [iff]: "space M \<in> sets M"
   3.110 +
   3.111 +lemma (in algebra) compl_sets [intro]:
   3.112 +  "a \<in> sets M \<Longrightarrow> space M - a \<in> sets M"
   3.113 +  by auto
   3.114 +
   3.115 +lemma algebra_iff_Un:
   3.116 +  "algebra M \<longleftrightarrow>
   3.117 +    sets M \<subseteq> Pow (space M) &
   3.118 +    {} \<in> sets M &
   3.119 +    (\<forall>a \<in> sets M. space M - a \<in> sets M) &
   3.120 +    (\<forall>a \<in> sets M. \<forall> b \<in> sets M. a \<union> b \<in> sets M)" (is "_ \<longleftrightarrow> ?Un")
   3.121 +proof
   3.122 +  assume "algebra M"
   3.123 +  then interpret algebra M .
   3.124 +  show ?Un using sets_into_space by auto
   3.125 +next
   3.126 +  assume ?Un
   3.127 +  show "algebra M"
   3.128 +  proof
   3.129 +    show space: "sets M \<subseteq> Pow (space M)" "{} \<in> sets M" "space M \<in> sets M"
   3.130 +      using `?Un` by auto
   3.131 +    fix a b assume a: "a \<in> sets M" and b: "b \<in> sets M"
   3.132 +    then show "a \<union> b \<in> sets M" using `?Un` by auto
   3.133 +    have "a - b = space M - ((space M - a) \<union> b)"
   3.134 +      using space a b by auto
   3.135 +    then show "a - b \<in> sets M"
   3.136 +      using a b  `?Un` by auto
   3.137 +  qed
   3.138 +qed
   3.139 +
   3.140 +lemma algebra_iff_Int:
   3.141 +     "algebra M \<longleftrightarrow>
   3.142 +       sets M \<subseteq> Pow (space M) & {} \<in> sets M &
   3.143 +       (\<forall>a \<in> sets M. space M - a \<in> sets M) &
   3.144 +       (\<forall>a \<in> sets M. \<forall> b \<in> sets M. a \<inter> b \<in> sets M)" (is "_ \<longleftrightarrow> ?Int")
   3.145 +proof
   3.146 +  assume "algebra M"
   3.147 +  then interpret algebra M .
   3.148 +  show ?Int using sets_into_space by auto
   3.149 +next
   3.150 +  assume ?Int
   3.151 +  show "algebra M"
   3.152 +  proof (unfold algebra_iff_Un, intro conjI ballI)
   3.153 +    show space: "sets M \<subseteq> Pow (space M)" "{} \<in> sets M"
   3.154 +      using `?Int` by auto
   3.155 +    from `?Int` show "\<And>a. a \<in> sets M \<Longrightarrow> space M - a \<in> sets M" by auto
   3.156 +    fix a b assume sets: "a \<in> sets M" "b \<in> sets M"
   3.157 +    hence "a \<union> b = space M - ((space M - a) \<inter> (space M - b))"
   3.158 +      using space by blast
   3.159 +    also have "... \<in> sets M"
   3.160 +      using sets `?Int` by auto
   3.161 +    finally show "a \<union> b \<in> sets M" .
   3.162 +  qed
   3.163 +qed
   3.164 +
   3.165  section {* Restricted algebras *}
   3.166  
   3.167  abbreviation (in algebra)
   3.168 @@ -174,7 +196,7 @@
   3.169  
   3.170  lemma algebra_Pow:
   3.171       "algebra \<lparr> space = sp, sets = Pow sp, \<dots> = X \<rparr>"
   3.172 -  by (auto simp add: algebra_def)
   3.173 +  by (auto simp add: algebra_iff_Un)
   3.174  
   3.175  lemma sigma_algebra_Pow:
   3.176       "sigma_algebra \<lparr> space = sp, sets = Pow sp, \<dots> = X \<rparr>"
   3.177 @@ -205,7 +227,7 @@
   3.178         {} \<in> sets M \<and> (\<forall>s \<in> sets M. space M - s \<in> sets M) \<and>
   3.179         (\<forall>A. range A \<subseteq> sets M \<longrightarrow> (\<Union>i::nat. A i) \<in> sets M)"
   3.180    by (auto simp add: range_binary_eq sigma_algebra_def sigma_algebra_axioms_def
   3.181 -         algebra_def Un_range_binary)
   3.182 +         algebra_iff_Un Un_range_binary)
   3.183  
   3.184  subsection {* Initial Sigma Algebra *}
   3.185  
   3.186 @@ -513,7 +535,7 @@
   3.187    thus "{x \<in> space M. x \<in> A} \<in> sets M" using `A \<in> sets M` by auto
   3.188  qed
   3.189  
   3.190 -lemma (in algebra) measurable_ident[intro, simp]: "id \<in> measurable M M"
   3.191 +lemma (in ring_of_sets) measurable_ident[intro, simp]: "id \<in> measurable M M"
   3.192    by (auto simp add: measurable_def)
   3.193  
   3.194  lemma measurable_comp[intro]:
   3.195 @@ -666,7 +688,7 @@
   3.196  lemma disjointed_subset: "disjointed A n \<subseteq> A n"
   3.197    by (auto simp add: disjointed_def)
   3.198  
   3.199 -lemma (in algebra) UNION_in_sets:
   3.200 +lemma (in ring_of_sets) UNION_in_sets:
   3.201    fixes A:: "nat \<Rightarrow> 'a set"
   3.202    assumes A: "range A \<subseteq> sets M "
   3.203    shows  "(\<Union>i\<in>{0..<n}. A i) \<in> sets M"
   3.204 @@ -678,7 +700,7 @@
   3.205      by (simp add: atLeastLessThanSuc) (metis A Un UNIV_I image_subset_iff)
   3.206  qed
   3.207  
   3.208 -lemma (in algebra) range_disjointed_sets:
   3.209 +lemma (in ring_of_sets) range_disjointed_sets:
   3.210    assumes A: "range A \<subseteq> sets M "
   3.211    shows  "range (disjointed A) \<subseteq> sets M"
   3.212  proof (auto simp add: disjointed_def)
   3.213 @@ -687,6 +709,10 @@
   3.214      by (metis A Diff UNIV_I image_subset_iff)
   3.215  qed
   3.216  
   3.217 +lemma (in algebra) range_disjointed_sets':
   3.218 +  "range A \<subseteq> sets M \<Longrightarrow> range (disjointed A) \<subseteq> sets M"
   3.219 +  using range_disjointed_sets .
   3.220 +
   3.221  lemma sigma_algebra_disjoint_iff:
   3.222       "sigma_algebra M \<longleftrightarrow>
   3.223        algebra M &
   3.224 @@ -702,7 +728,7 @@
   3.225           disjoint_family (disjointed A) \<longrightarrow>
   3.226           (\<Union>i. disjointed A i) \<in> sets M" by blast
   3.227    hence "(\<Union>i. disjointed A i) \<in> sets M"
   3.228 -    by (simp add: algebra.range_disjointed_sets M A disjoint_family_disjointed)
   3.229 +    by (simp add: algebra.range_disjointed_sets' M A disjoint_family_disjointed)
   3.230    thus "(\<Union>i::nat. A i) \<in> sets M" by (simp add: UN_disjointed_eq)
   3.231  qed
   3.232  
   3.233 @@ -868,7 +894,6 @@
   3.234          (\<Union>i. A i) \<in> sets M) &
   3.235     (\<forall>A. (range A \<subseteq> sets M) & disjoint_family A \<longrightarrow> (\<Union>i::nat. A i) \<in> sets M)"
   3.236  
   3.237 -
   3.238  inductive_set
   3.239    smallest_ccdi_sets :: "('a, 'b) algebra_scheme \<Rightarrow> 'a set set"
   3.240    for M
   3.241 @@ -1117,17 +1142,12 @@
   3.242  
   3.243  section {* Dynkin systems *}
   3.244  
   3.245 -locale dynkin_system =
   3.246 -  fixes M :: "('a, 'b) algebra_scheme"
   3.247 -  assumes space_closed: "sets M \<subseteq> Pow (space M)"
   3.248 -    and   space: "space M \<in> sets M"
   3.249 +locale dynkin_system = subset_class +
   3.250 +  assumes space: "space M \<in> sets M"
   3.251      and   compl[intro!]: "\<And>A. A \<in> sets M \<Longrightarrow> space M - A \<in> sets M"
   3.252      and   UN[intro!]: "\<And>A. disjoint_family A \<Longrightarrow> range A \<subseteq> sets M
   3.253                             \<Longrightarrow> (\<Union>i::nat. A i) \<in> sets M"
   3.254  
   3.255 -lemma (in dynkin_system) sets_into_space: "\<And> A. A \<in> sets M \<Longrightarrow> A \<subseteq> space M"
   3.256 -  using space_closed by auto
   3.257 -
   3.258  lemma (in dynkin_system) empty[intro, simp]: "{} \<in> sets M"
   3.259    using space compl[of "space M"] by simp
   3.260  
   3.261 @@ -1156,7 +1176,7 @@
   3.262    assumes "\<And> A. disjoint_family A \<Longrightarrow> range A \<subseteq> sets M
   3.263            \<Longrightarrow> (\<Union>i::nat. A i) \<in> sets M"
   3.264    shows "dynkin_system M"
   3.265 -  using assms by (auto simp: dynkin_system_def)
   3.266 +  using assms by (auto simp: dynkin_system_def dynkin_system_axioms_def subset_class_def)
   3.267  
   3.268  lemma dynkin_system_trivial:
   3.269    shows "dynkin_system \<lparr> space = A, sets = Pow A \<rparr>"
   3.270 @@ -1184,7 +1204,7 @@
   3.271  next
   3.272    assume "Int_stable M"
   3.273    show "sigma_algebra M"
   3.274 -    unfolding sigma_algebra_disjoint_iff algebra_def
   3.275 +    unfolding sigma_algebra_disjoint_iff algebra_iff_Un
   3.276    proof (intro conjI ballI allI impI)
   3.277      show "sets M \<subseteq> Pow (space M)" using sets_into_space by auto
   3.278    next
   3.279 @@ -1211,13 +1231,12 @@
   3.280    fix A assume "A \<in> sets (dynkin M)"
   3.281    moreover
   3.282    { fix D assume "A \<in> D" and d: "dynkin_system \<lparr> space = space M, sets = D \<rparr>"
   3.283 -    from dynkin_system.sets_into_space[OF d] `A \<in> D`
   3.284 -    have "A \<subseteq> space M" by auto }
   3.285 +    then have "A \<subseteq> space M" by (auto simp: dynkin_system_def subset_class_def) }
   3.286    moreover have "{D. dynkin_system \<lparr> space = space M, sets = D\<rparr> \<and> sets M \<subseteq> D} \<noteq> {}"
   3.287      using assms dynkin_system_trivial by fastsimp
   3.288    ultimately show "A \<subseteq> space (dynkin M)"
   3.289      unfolding dynkin_def using assms
   3.290 -    by simp (metis dynkin_system.sets_into_space in_mono mem_def)
   3.291 +    by simp (metis dynkin_system_def subset_class_def in_mono mem_def)
   3.292  next
   3.293    show "space (dynkin M) \<in> sets (dynkin M)"
   3.294      unfolding dynkin_def using dynkin_system.space by fastsimp
   3.295 @@ -1277,7 +1296,7 @@
   3.296  proof -
   3.297    have "dynkin_system M" by default
   3.298    then have "dynkin_system \<lparr>space = space N, sets = sets M \<rparr>"
   3.299 -    using assms unfolding dynkin_system_def by simp
   3.300 +    using assms unfolding dynkin_system_def dynkin_system_axioms_def subset_class_def by simp
   3.301    with `sets N \<subseteq> sets M` show ?thesis by (auto simp add: dynkin_def)
   3.302  qed
   3.303