13 definitions in classical mathematics. We define the least @{text |
13 definitions in classical mathematics. We define the least @{text |
14 \<sigma>}-algebra over a given set of sets. |
14 \<sigma>}-algebra over a given set of sets. |
15 *} |
15 *} |
16 |
16 |
17 consts |
17 consts |
18 sigma_algebra :: "'a set set => 'a set set" ("\<sigma>'_algebra") |
18 \<sigma>_algebra :: "'a set set => 'a set set" |
19 |
19 |
20 inductive "\<sigma>_algebra A" |
20 inductive "\<sigma>_algebra A" |
21 intros |
21 intros |
22 basic: "a \<in> A ==> a \<in> \<sigma>_algebra A" |
22 basic: "a \<in> A ==> a \<in> \<sigma>_algebra A" |
23 UNIV: "UNIV \<in> \<sigma>_algebra A" |
23 UNIV: "UNIV \<in> \<sigma>_algebra A" |
30 no induction nor cases. |
30 no induction nor cases. |
31 *} |
31 *} |
32 |
32 |
33 theorem sigma_algebra_empty: "{} \<in> \<sigma>_algebra A" |
33 theorem sigma_algebra_empty: "{} \<in> \<sigma>_algebra A" |
34 proof - |
34 proof - |
35 have "UNIV \<in> \<sigma>_algebra A" by (rule sigma_algebra.UNIV) |
35 have "UNIV \<in> \<sigma>_algebra A" by (rule \<sigma>_algebra.UNIV) |
36 hence "-UNIV \<in> \<sigma>_algebra A" by (rule sigma_algebra.complement) |
36 hence "-UNIV \<in> \<sigma>_algebra A" by (rule \<sigma>_algebra.complement) |
37 also have "-UNIV = {}" by simp |
37 also have "-UNIV = {}" by simp |
38 finally show ?thesis . |
38 finally show ?thesis . |
39 qed |
39 qed |
40 |
40 |
41 theorem sigma_algebra_Inter: |
41 theorem sigma_algebra_Inter: |
42 "(!!i::nat. a i \<in> \<sigma>_algebra A) ==> (\<Inter>i. a i) \<in> \<sigma>_algebra A" |
42 "(!!i::nat. a i \<in> \<sigma>_algebra A) ==> (\<Inter>i. a i) \<in> \<sigma>_algebra A" |
43 proof - |
43 proof - |
44 assume "!!i::nat. a i \<in> \<sigma>_algebra A" |
44 assume "!!i::nat. a i \<in> \<sigma>_algebra A" |
45 hence "!!i::nat. -(a i) \<in> \<sigma>_algebra A" by (rule sigma_algebra.complement) |
45 hence "!!i::nat. -(a i) \<in> \<sigma>_algebra A" by (rule \<sigma>_algebra.complement) |
46 hence "(\<Union>i. -(a i)) \<in> \<sigma>_algebra A" by (rule sigma_algebra.Union) |
46 hence "(\<Union>i. -(a i)) \<in> \<sigma>_algebra A" by (rule \<sigma>_algebra.Union) |
47 hence "-(\<Union>i. -(a i)) \<in> \<sigma>_algebra A" by (rule sigma_algebra.complement) |
47 hence "-(\<Union>i. -(a i)) \<in> \<sigma>_algebra A" by (rule \<sigma>_algebra.complement) |
48 also have "-(\<Union>i. -(a i)) = (\<Inter>i. a i)" by simp |
48 also have "-(\<Union>i. -(a i)) = (\<Inter>i. a i)" by simp |
49 finally show ?thesis . |
49 finally show ?thesis . |
50 qed |
50 qed |
51 |
51 |
52 end |
52 end |