2 Author: Markus Wenzel, TU Muenchen |
2 Author: Markus Wenzel, TU Muenchen |
3 *) |
3 *) |
4 |
4 |
5 header {* Sigma algebras *} |
5 header {* Sigma algebras *} |
6 |
6 |
7 theory Sigma_Algebra imports Main begin |
7 theory Sigma_Algebra |
|
8 imports Main |
|
9 begin |
8 |
10 |
9 text {* |
11 text {* |
10 This is just a tiny example demonstrating the use of inductive |
12 This is just a tiny example demonstrating the use of inductive |
11 definitions in classical mathematics. We define the least @{text |
13 definitions in classical mathematics. We define the least @{text |
12 \<sigma>}-algebra over a given set of sets. |
14 \<sigma>}-algebra over a given set of sets. |
13 *} |
15 *} |
14 |
16 |
15 inductive_set |
17 inductive_set \<sigma>_algebra :: "'a set set => 'a set set" for A :: "'a set set" |
16 \<sigma>_algebra :: "'a set set => 'a set set" |
18 where |
17 for A :: "'a set set" |
19 basic: "a \<in> A ==> a \<in> \<sigma>_algebra A" |
18 where |
20 | UNIV: "UNIV \<in> \<sigma>_algebra A" |
19 basic: "a \<in> A ==> a \<in> \<sigma>_algebra A" |
21 | complement: "a \<in> \<sigma>_algebra A ==> -a \<in> \<sigma>_algebra A" |
20 | UNIV: "UNIV \<in> \<sigma>_algebra A" |
22 | Union: "(!!i::nat. a i \<in> \<sigma>_algebra A) ==> (\<Union>i. a i) \<in> \<sigma>_algebra A" |
21 | complement: "a \<in> \<sigma>_algebra A ==> -a \<in> \<sigma>_algebra A" |
|
22 | Union: "(!!i::nat. a i \<in> \<sigma>_algebra A) ==> (\<Union>i. a i) \<in> \<sigma>_algebra A" |
|
23 |
23 |
24 text {* |
24 text {* |
25 The following basic facts are consequences of the closure properties |
25 The following basic facts are consequences of the closure properties |
26 of any @{text \<sigma>}-algebra, merely using the introduction rules, but |
26 of any @{text \<sigma>}-algebra, merely using the introduction rules, but |
27 no induction nor cases. |
27 no induction nor cases. |
28 *} |
28 *} |
29 |
29 |
30 theorem sigma_algebra_empty: "{} \<in> \<sigma>_algebra A" |
30 theorem sigma_algebra_empty: "{} \<in> \<sigma>_algebra A" |
31 proof - |
31 proof - |
32 have "UNIV \<in> \<sigma>_algebra A" by (rule \<sigma>_algebra.UNIV) |
32 have "UNIV \<in> \<sigma>_algebra A" by (rule \<sigma>_algebra.UNIV) |
33 hence "-UNIV \<in> \<sigma>_algebra A" by (rule \<sigma>_algebra.complement) |
33 then have "-UNIV \<in> \<sigma>_algebra A" by (rule \<sigma>_algebra.complement) |
34 also have "-UNIV = {}" by simp |
34 also have "-UNIV = {}" by simp |
35 finally show ?thesis . |
35 finally show ?thesis . |
36 qed |
36 qed |
37 |
37 |
38 theorem sigma_algebra_Inter: |
38 theorem sigma_algebra_Inter: |
39 "(!!i::nat. a i \<in> \<sigma>_algebra A) ==> (\<Inter>i. a i) \<in> \<sigma>_algebra A" |
39 "(!!i::nat. a i \<in> \<sigma>_algebra A) ==> (\<Inter>i. a i) \<in> \<sigma>_algebra A" |
40 proof - |
40 proof - |
41 assume "!!i::nat. a i \<in> \<sigma>_algebra A" |
41 assume "!!i::nat. a i \<in> \<sigma>_algebra A" |
42 hence "!!i::nat. -(a i) \<in> \<sigma>_algebra A" by (rule \<sigma>_algebra.complement) |
42 then have "!!i::nat. -(a i) \<in> \<sigma>_algebra A" by (rule \<sigma>_algebra.complement) |
43 hence "(\<Union>i. -(a i)) \<in> \<sigma>_algebra A" by (rule \<sigma>_algebra.Union) |
43 then have "(\<Union>i. -(a i)) \<in> \<sigma>_algebra A" by (rule \<sigma>_algebra.Union) |
44 hence "-(\<Union>i. -(a i)) \<in> \<sigma>_algebra A" by (rule \<sigma>_algebra.complement) |
44 then have "-(\<Union>i. -(a i)) \<in> \<sigma>_algebra A" by (rule \<sigma>_algebra.complement) |
45 also have "-(\<Union>i. -(a i)) = (\<Inter>i. a i)" by simp |
45 also have "-(\<Union>i. -(a i)) = (\<Inter>i. a i)" by simp |
46 finally show ?thesis . |
46 finally show ?thesis . |
47 qed |
47 qed |
48 |
48 |
49 end |
49 end |