equal
deleted
inserted
replaced
4 *) |
4 *) |
5 |
5 |
6 header {*Borel spaces*} |
6 header {*Borel spaces*} |
7 |
7 |
8 theory Borel_Space |
8 theory Borel_Space |
9 imports Sigma_Algebra "~~/src/HOL/Multivariate_Analysis/Multivariate_Analysis" |
9 imports |
|
10 Measurable |
|
11 "~~/src/HOL/Multivariate_Analysis/Multivariate_Analysis" |
10 begin |
12 begin |
11 |
13 |
12 section "Generic Borel spaces" |
14 section "Generic Borel spaces" |
13 |
15 |
14 definition borel :: "'a::topological_space measure" where |
16 definition borel :: "'a::topological_space measure" where |
31 unfolding borel_def by auto |
33 unfolding borel_def by auto |
32 |
34 |
33 lemma space_in_borel[measurable]: "UNIV \<in> sets borel" |
35 lemma space_in_borel[measurable]: "UNIV \<in> sets borel" |
34 unfolding borel_def by auto |
36 unfolding borel_def by auto |
35 |
37 |
36 lemma pred_Collect_borel[measurable (raw)]: "Sigma_Algebra.pred borel P \<Longrightarrow> {x. P x} \<in> sets borel" |
38 lemma pred_Collect_borel[measurable (raw)]: "Measurable.pred borel P \<Longrightarrow> {x. P x} \<in> sets borel" |
37 unfolding borel_def pred_def by auto |
39 unfolding borel_def pred_def by auto |
38 |
40 |
39 lemma borel_open[measurable (raw generic)]: |
41 lemma borel_open[measurable (raw generic)]: |
40 assumes "open A" shows "A \<in> sets borel" |
42 assumes "open A" shows "A \<in> sets borel" |
41 proof - |
43 proof - |