22 it is often not possible to consistently assign a measure to every |
22 it is often not possible to consistently assign a measure to every |
23 subset. Therefore it is necessary to define the set of measurable |
23 subset. Therefore it is necessary to define the set of measurable |
24 subsets of the universe. A sigma algebra is such a set that has |
24 subsets of the universe. A sigma algebra is such a set that has |
25 three very natural and desirable properties. *} |
25 three very natural and desirable properties. *} |
26 |
26 |
27 subsection {* Algebras *} |
27 subsection {* Families of sets *} |
28 |
28 |
29 locale subset_class = |
29 locale subset_class = |
30 fixes \<Omega> :: "'a set" and M :: "'a set set" |
30 fixes \<Omega> :: "'a set" and M :: "'a set set" |
31 assumes space_closed: "M \<subseteq> Pow \<Omega>" |
31 assumes space_closed: "M \<subseteq> Pow \<Omega>" |
32 |
32 |
33 lemma (in subset_class) sets_into_space: "x \<in> M \<Longrightarrow> x \<subseteq> \<Omega>" |
33 lemma (in subset_class) sets_into_space: "x \<in> M \<Longrightarrow> x \<subseteq> \<Omega>" |
34 by (metis PowD contra_subsetD space_closed) |
34 by (metis PowD contra_subsetD space_closed) |
35 |
35 |
36 locale ring_of_sets = subset_class + |
36 subsection {* Semiring of sets *} |
37 assumes empty_sets [iff]: "{} \<in> M" |
37 |
38 and Diff [intro]: "\<And>a b. a \<in> M \<Longrightarrow> b \<in> M \<Longrightarrow> a - b \<in> M" |
38 subsubsection {* Disjoint sets *} |
39 and Un [intro]: "\<And>a b. a \<in> M \<Longrightarrow> b \<in> M \<Longrightarrow> a \<union> b \<in> M" |
39 |
40 |
40 definition "disjoint A \<longleftrightarrow> (\<forall>a\<in>A. \<forall>b\<in>A. a \<noteq> b \<longrightarrow> a \<inter> b = {})" |
41 lemma (in ring_of_sets) Int [intro]: |
41 |
42 assumes a: "a \<in> M" and b: "b \<in> M" shows "a \<inter> b \<in> M" |
42 lemma disjointI: |
43 proof - |
43 "(\<And>a b. a \<in> A \<Longrightarrow> b \<in> A \<Longrightarrow> a \<noteq> b \<Longrightarrow> a \<inter> b = {}) \<Longrightarrow> disjoint A" |
44 have "a \<inter> b = a - (a - b)" |
44 unfolding disjoint_def by auto |
|
45 |
|
46 lemma disjointD: |
|
47 "disjoint A \<Longrightarrow> a \<in> A \<Longrightarrow> b \<in> A \<Longrightarrow> a \<noteq> b \<Longrightarrow> a \<inter> b = {}" |
|
48 unfolding disjoint_def by auto |
|
49 |
|
50 lemma disjoint_empty[iff]: "disjoint {}" |
|
51 by (auto simp: disjoint_def) |
|
52 |
|
53 lemma disjoint_union: |
|
54 assumes C: "disjoint C" and B: "disjoint B" and disj: "\<Union>C \<inter> \<Union>B = {}" |
|
55 shows "disjoint (C \<union> B)" |
|
56 proof (rule disjointI) |
|
57 fix c d assume sets: "c \<in> C \<union> B" "d \<in> C \<union> B" and "c \<noteq> d" |
|
58 show "c \<inter> d = {}" |
|
59 proof cases |
|
60 assume "(c \<in> C \<and> d \<in> C) \<or> (c \<in> B \<and> d \<in> B)" |
|
61 then show ?thesis |
|
62 proof |
|
63 assume "c \<in> C \<and> d \<in> C" with `c \<noteq> d` C show "c \<inter> d = {}" |
|
64 by (auto simp: disjoint_def) |
|
65 next |
|
66 assume "c \<in> B \<and> d \<in> B" with `c \<noteq> d` B show "c \<inter> d = {}" |
|
67 by (auto simp: disjoint_def) |
|
68 qed |
|
69 next |
|
70 assume "\<not> ((c \<in> C \<and> d \<in> C) \<or> (c \<in> B \<and> d \<in> B))" |
|
71 with sets have "(c \<subseteq> \<Union>C \<and> d \<subseteq> \<Union>B) \<or> (c \<subseteq> \<Union>B \<and> d \<subseteq> \<Union>C)" |
|
72 by auto |
|
73 with disj show "c \<inter> d = {}" by auto |
|
74 qed |
|
75 qed |
|
76 |
|
77 locale semiring_of_sets = subset_class + |
|
78 assumes empty_sets[iff]: "{} \<in> M" |
|
79 assumes Int[intro]: "\<And>a b. a \<in> M \<Longrightarrow> b \<in> M \<Longrightarrow> a \<inter> b \<in> M" |
|
80 assumes Diff_cover: |
|
81 "\<And>a b. a \<in> M \<Longrightarrow> b \<in> M \<Longrightarrow> \<exists>C\<subseteq>M. finite C \<and> disjoint C \<and> a - b = \<Union>C" |
|
82 |
|
83 lemma (in semiring_of_sets) finite_INT[intro]: |
|
84 assumes "finite I" "I \<noteq> {}" "\<And>i. i \<in> I \<Longrightarrow> A i \<in> M" |
|
85 shows "(\<Inter>i\<in>I. A i) \<in> M" |
|
86 using assms by (induct rule: finite_ne_induct) auto |
|
87 |
|
88 lemma (in semiring_of_sets) Int_space_eq1 [simp]: "x \<in> M \<Longrightarrow> \<Omega> \<inter> x = x" |
|
89 by (metis Int_absorb1 sets_into_space) |
|
90 |
|
91 lemma (in semiring_of_sets) Int_space_eq2 [simp]: "x \<in> M \<Longrightarrow> x \<inter> \<Omega> = x" |
|
92 by (metis Int_absorb2 sets_into_space) |
|
93 |
|
94 lemma (in semiring_of_sets) sets_Collect_conj: |
|
95 assumes "{x\<in>\<Omega>. P x} \<in> M" "{x\<in>\<Omega>. Q x} \<in> M" |
|
96 shows "{x\<in>\<Omega>. Q x \<and> P x} \<in> M" |
|
97 proof - |
|
98 have "{x\<in>\<Omega>. Q x \<and> P x} = {x\<in>\<Omega>. Q x} \<inter> {x\<in>\<Omega>. P x}" |
45 by auto |
99 by auto |
46 then show "a \<inter> b \<in> M" |
100 with assms show ?thesis by auto |
47 using a b by auto |
101 qed |
48 qed |
102 |
|
103 lemma (in semiring_of_sets) sets_Collect_finite_All: |
|
104 assumes "\<And>i. i \<in> S \<Longrightarrow> {x\<in>\<Omega>. P i x} \<in> M" "finite S" "S \<noteq> {}" |
|
105 shows "{x\<in>\<Omega>. \<forall>i\<in>S. P i x} \<in> M" |
|
106 proof - |
|
107 have "{x\<in>\<Omega>. \<forall>i\<in>S. P i x} = (\<Inter>i\<in>S. {x\<in>\<Omega>. P i x})" |
|
108 using `S \<noteq> {}` by auto |
|
109 with assms show ?thesis by auto |
|
110 qed |
|
111 |
|
112 locale ring_of_sets = semiring_of_sets + |
|
113 assumes Un [intro]: "\<And>a b. a \<in> M \<Longrightarrow> b \<in> M \<Longrightarrow> a \<union> b \<in> M" |
49 |
114 |
50 lemma (in ring_of_sets) finite_Union [intro]: |
115 lemma (in ring_of_sets) finite_Union [intro]: |
51 "finite X \<Longrightarrow> X \<subseteq> M \<Longrightarrow> Union X \<in> M" |
116 "finite X \<Longrightarrow> X \<subseteq> M \<Longrightarrow> Union X \<in> M" |
52 by (induct set: finite) (auto simp add: Un) |
117 by (induct set: finite) (auto simp add: Un) |
53 |
118 |
54 lemma (in ring_of_sets) finite_UN[intro]: |
119 lemma (in ring_of_sets) finite_UN[intro]: |
55 assumes "finite I" and "\<And>i. i \<in> I \<Longrightarrow> A i \<in> M" |
120 assumes "finite I" and "\<And>i. i \<in> I \<Longrightarrow> A i \<in> M" |
56 shows "(\<Union>i\<in>I. A i) \<in> M" |
121 shows "(\<Union>i\<in>I. A i) \<in> M" |
57 using assms by induct auto |
122 using assms by induct auto |
58 |
123 |
59 lemma (in ring_of_sets) finite_INT[intro]: |
124 lemma (in ring_of_sets) Diff [intro]: |
60 assumes "finite I" "I \<noteq> {}" "\<And>i. i \<in> I \<Longrightarrow> A i \<in> M" |
125 assumes "a \<in> M" "b \<in> M" shows "a - b \<in> M" |
61 shows "(\<Inter>i\<in>I. A i) \<in> M" |
126 using Diff_cover[OF assms] by auto |
62 using assms by (induct rule: finite_ne_induct) auto |
127 |
|
128 lemma ring_of_setsI: |
|
129 assumes space_closed: "M \<subseteq> Pow \<Omega>" |
|
130 assumes empty_sets[iff]: "{} \<in> M" |
|
131 assumes Un[intro]: "\<And>a b. a \<in> M \<Longrightarrow> b \<in> M \<Longrightarrow> a \<union> b \<in> M" |
|
132 assumes Diff[intro]: "\<And>a b. a \<in> M \<Longrightarrow> b \<in> M \<Longrightarrow> a - b \<in> M" |
|
133 shows "ring_of_sets \<Omega> M" |
|
134 proof |
|
135 fix a b assume ab: "a \<in> M" "b \<in> M" |
|
136 from ab show "\<exists>C\<subseteq>M. finite C \<and> disjoint C \<and> a - b = \<Union>C" |
|
137 by (intro exI[of _ "{a - b}"]) (auto simp: disjoint_def) |
|
138 have "a \<inter> b = a - (a - b)" by auto |
|
139 also have "\<dots> \<in> M" using ab by auto |
|
140 finally show "a \<inter> b \<in> M" . |
|
141 qed fact+ |
|
142 |
|
143 lemma ring_of_sets_iff: "ring_of_sets \<Omega> M \<longleftrightarrow> M \<subseteq> Pow \<Omega> \<and> {} \<in> M \<and> (\<forall>a\<in>M. \<forall>b\<in>M. a \<union> b \<in> M) \<and> (\<forall>a\<in>M. \<forall>b\<in>M. a - b \<in> M)" |
|
144 proof |
|
145 assume "ring_of_sets \<Omega> M" |
|
146 then interpret ring_of_sets \<Omega> M . |
|
147 show "M \<subseteq> Pow \<Omega> \<and> {} \<in> M \<and> (\<forall>a\<in>M. \<forall>b\<in>M. a \<union> b \<in> M) \<and> (\<forall>a\<in>M. \<forall>b\<in>M. a - b \<in> M)" |
|
148 using space_closed by auto |
|
149 qed (auto intro!: ring_of_setsI) |
63 |
150 |
64 lemma (in ring_of_sets) insert_in_sets: |
151 lemma (in ring_of_sets) insert_in_sets: |
65 assumes "{x} \<in> M" "A \<in> M" shows "insert x A \<in> M" |
152 assumes "{x} \<in> M" "A \<in> M" shows "insert x A \<in> M" |
66 proof - |
153 proof - |
67 have "{x} \<union> A \<in> M" using assms by (rule Un) |
154 have "{x} \<union> A \<in> M" using assms by (rule Un) |
68 thus ?thesis by auto |
155 thus ?thesis by auto |
69 qed |
|
70 |
|
71 lemma (in ring_of_sets) Int_space_eq1 [simp]: "x \<in> M \<Longrightarrow> \<Omega> \<inter> x = x" |
|
72 by (metis Int_absorb1 sets_into_space) |
|
73 |
|
74 lemma (in ring_of_sets) Int_space_eq2 [simp]: "x \<in> M \<Longrightarrow> x \<inter> \<Omega> = x" |
|
75 by (metis Int_absorb2 sets_into_space) |
|
76 |
|
77 lemma (in ring_of_sets) sets_Collect_conj: |
|
78 assumes "{x\<in>\<Omega>. P x} \<in> M" "{x\<in>\<Omega>. Q x} \<in> M" |
|
79 shows "{x\<in>\<Omega>. Q x \<and> P x} \<in> M" |
|
80 proof - |
|
81 have "{x\<in>\<Omega>. Q x \<and> P x} = {x\<in>\<Omega>. Q x} \<inter> {x\<in>\<Omega>. P x}" |
|
82 by auto |
|
83 with assms show ?thesis by auto |
|
84 qed |
156 qed |
85 |
157 |
86 lemma (in ring_of_sets) sets_Collect_disj: |
158 lemma (in ring_of_sets) sets_Collect_disj: |
87 assumes "{x\<in>\<Omega>. P x} \<in> M" "{x\<in>\<Omega>. Q x} \<in> M" |
159 assumes "{x\<in>\<Omega>. P x} \<in> M" "{x\<in>\<Omega>. Q x} \<in> M" |
88 shows "{x\<in>\<Omega>. Q x \<or> P x} \<in> M" |
160 shows "{x\<in>\<Omega>. Q x \<or> P x} \<in> M" |
89 proof - |
161 proof - |
90 have "{x\<in>\<Omega>. Q x \<or> P x} = {x\<in>\<Omega>. Q x} \<union> {x\<in>\<Omega>. P x}" |
162 have "{x\<in>\<Omega>. Q x \<or> P x} = {x\<in>\<Omega>. Q x} \<union> {x\<in>\<Omega>. P x}" |
91 by auto |
163 by auto |
92 with assms show ?thesis by auto |
|
93 qed |
|
94 |
|
95 lemma (in ring_of_sets) sets_Collect_finite_All: |
|
96 assumes "\<And>i. i \<in> S \<Longrightarrow> {x\<in>\<Omega>. P i x} \<in> M" "finite S" "S \<noteq> {}" |
|
97 shows "{x\<in>\<Omega>. \<forall>i\<in>S. P i x} \<in> M" |
|
98 proof - |
|
99 have "{x\<in>\<Omega>. \<forall>i\<in>S. P i x} = (\<Inter>i\<in>S. {x\<in>\<Omega>. P i x})" |
|
100 using `S \<noteq> {}` by auto |
|
101 with assms show ?thesis by auto |
164 with assms show ?thesis by auto |
102 qed |
165 qed |
103 |
166 |
104 lemma (in ring_of_sets) sets_Collect_finite_Ex: |
167 lemma (in ring_of_sets) sets_Collect_finite_Ex: |
105 assumes "\<And>i. i \<in> S \<Longrightarrow> {x\<in>\<Omega>. P i x} \<in> M" "finite S" |
168 assumes "\<And>i. i \<in> S \<Longrightarrow> {x\<in>\<Omega>. P i x} \<in> M" "finite S" |
760 hence "(\<Union>i. disjointed A i) \<in> M" |
839 hence "(\<Union>i. disjointed A i) \<in> M" |
761 by (simp add: algebra.range_disjointed_sets'[of \<Omega>] M A disjoint_family_disjointed) |
840 by (simp add: algebra.range_disjointed_sets'[of \<Omega>] M A disjoint_family_disjointed) |
762 thus "(\<Union>i::nat. A i) \<in> M" by (simp add: UN_disjointed_eq) |
841 thus "(\<Union>i::nat. A i) \<in> M" by (simp add: UN_disjointed_eq) |
763 qed |
842 qed |
764 |
843 |
|
844 lemma disjoint_family_on_disjoint_image: |
|
845 "disjoint_family_on A I \<Longrightarrow> disjoint (A ` I)" |
|
846 unfolding disjoint_family_on_def disjoint_def by force |
|
847 |
|
848 lemma disjoint_image_disjoint_family_on: |
|
849 assumes d: "disjoint (A ` I)" and i: "inj_on A I" |
|
850 shows "disjoint_family_on A I" |
|
851 unfolding disjoint_family_on_def |
|
852 proof (intro ballI impI) |
|
853 fix n m assume nm: "m \<in> I" "n \<in> I" and "n \<noteq> m" |
|
854 with i[THEN inj_onD, of n m] show "A n \<inter> A m = {}" |
|
855 by (intro disjointD[OF d]) auto |
|
856 qed |
|
857 |
|
858 section {* Ring generated by a semiring *} |
|
859 |
|
860 definition (in semiring_of_sets) |
|
861 "generated_ring = { \<Union>C | C. C \<subseteq> M \<and> finite C \<and> disjoint C }" |
|
862 |
|
863 lemma (in semiring_of_sets) generated_ringE[elim?]: |
|
864 assumes "a \<in> generated_ring" |
|
865 obtains C where "finite C" "disjoint C" "C \<subseteq> M" "a = \<Union>C" |
|
866 using assms unfolding generated_ring_def by auto |
|
867 |
|
868 lemma (in semiring_of_sets) generated_ringI[intro?]: |
|
869 assumes "finite C" "disjoint C" "C \<subseteq> M" "a = \<Union>C" |
|
870 shows "a \<in> generated_ring" |
|
871 using assms unfolding generated_ring_def by auto |
|
872 |
|
873 lemma (in semiring_of_sets) generated_ringI_Basic: |
|
874 "A \<in> M \<Longrightarrow> A \<in> generated_ring" |
|
875 by (rule generated_ringI[of "{A}"]) (auto simp: disjoint_def) |
|
876 |
|
877 lemma (in semiring_of_sets) generated_ring_disjoint_Un[intro]: |
|
878 assumes a: "a \<in> generated_ring" and b: "b \<in> generated_ring" |
|
879 and "a \<inter> b = {}" |
|
880 shows "a \<union> b \<in> generated_ring" |
|
881 proof - |
|
882 from a guess Ca .. note Ca = this |
|
883 from b guess Cb .. note Cb = this |
|
884 show ?thesis |
|
885 proof |
|
886 show "disjoint (Ca \<union> Cb)" |
|
887 using `a \<inter> b = {}` Ca Cb by (auto intro!: disjoint_union) |
|
888 qed (insert Ca Cb, auto) |
|
889 qed |
|
890 |
|
891 lemma (in semiring_of_sets) generated_ring_empty: "{} \<in> generated_ring" |
|
892 by (auto simp: generated_ring_def disjoint_def) |
|
893 |
|
894 lemma (in semiring_of_sets) generated_ring_disjoint_Union: |
|
895 assumes "finite A" shows "A \<subseteq> generated_ring \<Longrightarrow> disjoint A \<Longrightarrow> \<Union>A \<in> generated_ring" |
|
896 using assms by (induct A) (auto simp: disjoint_def intro!: generated_ring_disjoint_Un generated_ring_empty) |
|
897 |
|
898 lemma (in semiring_of_sets) generated_ring_disjoint_UNION: |
|
899 "finite I \<Longrightarrow> disjoint (A ` I) \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> A i \<in> generated_ring) \<Longrightarrow> UNION I A \<in> generated_ring" |
|
900 unfolding SUP_def by (intro generated_ring_disjoint_Union) auto |
|
901 |
|
902 lemma (in semiring_of_sets) generated_ring_Int: |
|
903 assumes a: "a \<in> generated_ring" and b: "b \<in> generated_ring" |
|
904 shows "a \<inter> b \<in> generated_ring" |
|
905 proof - |
|
906 from a guess Ca .. note Ca = this |
|
907 from b guess Cb .. note Cb = this |
|
908 def C \<equiv> "(\<lambda>(a,b). a \<inter> b)` (Ca\<times>Cb)" |
|
909 show ?thesis |
|
910 proof |
|
911 show "disjoint C" |
|
912 proof (simp add: disjoint_def C_def, intro ballI impI) |
|
913 fix a1 b1 a2 b2 assume sets: "a1 \<in> Ca" "b1 \<in> Cb" "a2 \<in> Ca" "b2 \<in> Cb" |
|
914 assume "a1 \<inter> b1 \<noteq> a2 \<inter> b2" |
|
915 then have "a1 \<noteq> a2 \<or> b1 \<noteq> b2" by auto |
|
916 then show "(a1 \<inter> b1) \<inter> (a2 \<inter> b2) = {}" |
|
917 proof |
|
918 assume "a1 \<noteq> a2" |
|
919 with sets Ca have "a1 \<inter> a2 = {}" |
|
920 by (auto simp: disjoint_def) |
|
921 then show ?thesis by auto |
|
922 next |
|
923 assume "b1 \<noteq> b2" |
|
924 with sets Cb have "b1 \<inter> b2 = {}" |
|
925 by (auto simp: disjoint_def) |
|
926 then show ?thesis by auto |
|
927 qed |
|
928 qed |
|
929 qed (insert Ca Cb, auto simp: C_def) |
|
930 qed |
|
931 |
|
932 lemma (in semiring_of_sets) generated_ring_Inter: |
|
933 assumes "finite A" "A \<noteq> {}" shows "A \<subseteq> generated_ring \<Longrightarrow> \<Inter>A \<in> generated_ring" |
|
934 using assms by (induct A rule: finite_ne_induct) (auto intro: generated_ring_Int) |
|
935 |
|
936 lemma (in semiring_of_sets) generated_ring_INTER: |
|
937 "finite I \<Longrightarrow> I \<noteq> {} \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> A i \<in> generated_ring) \<Longrightarrow> INTER I A \<in> generated_ring" |
|
938 unfolding INF_def by (intro generated_ring_Inter) auto |
|
939 |
|
940 lemma (in semiring_of_sets) generating_ring: |
|
941 "ring_of_sets \<Omega> generated_ring" |
|
942 proof (rule ring_of_setsI) |
|
943 let ?R = generated_ring |
|
944 show "?R \<subseteq> Pow \<Omega>" |
|
945 using sets_into_space by (auto simp: generated_ring_def generated_ring_empty) |
|
946 show "{} \<in> ?R" by (rule generated_ring_empty) |
|
947 |
|
948 { fix a assume a: "a \<in> ?R" then guess Ca .. note Ca = this |
|
949 fix b assume b: "b \<in> ?R" then guess Cb .. note Cb = this |
|
950 |
|
951 show "a - b \<in> ?R" |
|
952 proof cases |
|
953 assume "Cb = {}" with Cb `a \<in> ?R` show ?thesis |
|
954 by simp |
|
955 next |
|
956 assume "Cb \<noteq> {}" |
|
957 with Ca Cb have "a - b = (\<Union>a'\<in>Ca. \<Inter>b'\<in>Cb. a' - b')" by auto |
|
958 also have "\<dots> \<in> ?R" |
|
959 proof (intro generated_ring_INTER generated_ring_disjoint_UNION) |
|
960 fix a b assume "a \<in> Ca" "b \<in> Cb" |
|
961 with Ca Cb Diff_cover[of a b] show "a - b \<in> ?R" |
|
962 by (auto simp add: generated_ring_def) |
|
963 next |
|
964 show "disjoint ((\<lambda>a'. \<Inter>b'\<in>Cb. a' - b')`Ca)" |
|
965 using Ca by (auto simp add: disjoint_def `Cb \<noteq> {}`) |
|
966 next |
|
967 show "finite Ca" "finite Cb" "Cb \<noteq> {}" by fact+ |
|
968 qed |
|
969 finally show "a - b \<in> ?R" . |
|
970 qed } |
|
971 note Diff = this |
|
972 |
|
973 fix a b assume sets: "a \<in> ?R" "b \<in> ?R" |
|
974 have "a \<union> b = (a - b) \<union> (a \<inter> b) \<union> (b - a)" by auto |
|
975 also have "\<dots> \<in> ?R" |
|
976 by (intro sets generated_ring_disjoint_Un generated_ring_Int Diff) auto |
|
977 finally show "a \<union> b \<in> ?R" . |
|
978 qed |
|
979 |
|
980 lemma (in semiring_of_sets) sigma_sets_generated_ring_eq: "sigma_sets \<Omega> generated_ring = sigma_sets \<Omega> M" |
|
981 proof |
|
982 interpret M: sigma_algebra \<Omega> "sigma_sets \<Omega> M" |
|
983 using space_closed by (rule sigma_algebra_sigma_sets) |
|
984 show "sigma_sets \<Omega> generated_ring \<subseteq> sigma_sets \<Omega> M" |
|
985 by (blast intro!: sigma_sets_mono elim: generated_ringE) |
|
986 qed (auto intro!: generated_ringI_Basic sigma_sets_mono) |
|
987 |
765 section {* Measure type *} |
988 section {* Measure type *} |
766 |
989 |
767 definition positive :: "'a set set \<Rightarrow> ('a set \<Rightarrow> ereal) \<Rightarrow> bool" where |
990 definition positive :: "'a set set \<Rightarrow> ('a set \<Rightarrow> ereal) \<Rightarrow> bool" where |
768 "positive M \<mu> \<longleftrightarrow> \<mu> {} = 0 \<and> (\<forall>A\<in>M. 0 \<le> \<mu> A)" |
991 "positive M \<mu> \<longleftrightarrow> \<mu> {} = 0 \<and> (\<forall>A\<in>M. 0 \<le> \<mu> A)" |
769 |
992 |