src/HOL/Analysis/Sigma_Algebra.thy
 changeset 68607 67bb59e49834 parent 68403 223172b97d0b child 69164 74f1b0f10b2b
     1.1 --- a/src/HOL/Analysis/Sigma_Algebra.thy	Mon Jul 09 21:55:40 2018 +0100
1.2 +++ b/src/HOL/Analysis/Sigma_Algebra.thy	Tue Jul 10 09:38:35 2018 +0200
1.3 @@ -146,13 +146,13 @@
1.4    "a \<in> M \<Longrightarrow> \<Omega> - a \<in> M"
1.5    by auto
1.6
1.7 -lemma%important algebra_iff_Un:
1.8 +proposition algebra_iff_Un:
1.9    "algebra \<Omega> M \<longleftrightarrow>
1.10      M \<subseteq> Pow \<Omega> \<and>
1.11      {} \<in> M \<and>
1.12      (\<forall>a \<in> M. \<Omega> - a \<in> M) \<and>
1.13      (\<forall>a \<in> M. \<forall> b \<in> M. a \<union> b \<in> M)" (is "_ \<longleftrightarrow> ?Un")
1.14 -proof%unimportant
1.15 +proof
1.16    assume "algebra \<Omega> M"
1.17    then interpret algebra \<Omega> M .
1.18    show ?Un using sets_into_space by auto
1.19 @@ -173,12 +173,12 @@
1.20    show "algebra \<Omega> M" proof qed fact
1.21  qed
1.22
1.23 -lemma%important algebra_iff_Int:
1.24 +proposition algebra_iff_Int:
1.25       "algebra \<Omega> M \<longleftrightarrow>
1.26         M \<subseteq> Pow \<Omega> & {} \<in> M &
1.27         (\<forall>a \<in> M. \<Omega> - a \<in> M) &
1.28         (\<forall>a \<in> M. \<forall> b \<in> M. a \<inter> b \<in> M)" (is "_ \<longleftrightarrow> ?Int")
1.29 -proof%unimportant
1.30 +proof
1.31    assume "algebra \<Omega> M"
1.32    then interpret algebra \<Omega> M .
1.33    show ?Int using sets_into_space by auto
1.34 @@ -1433,7 +1433,7 @@
1.35  text%important \<open>The reason to introduce Dynkin-systems is the following induction rules for $\sigma$-algebras
1.36  generated by a generator closed under intersection.\<close>
1.37
1.38 -lemma%important sigma_sets_induct_disjoint[consumes 3, case_names basic empty compl union]:
1.39 +proposition sigma_sets_induct_disjoint[consumes 3, case_names basic empty compl union]:
1.40    assumes "Int_stable G"
1.41      and closed: "G \<subseteq> Pow \<Omega>"
1.42      and A: "A \<in> sigma_sets \<Omega> G"
1.43 @@ -1442,7 +1442,7 @@
1.44      and compl: "\<And>A. A \<in> sigma_sets \<Omega> G \<Longrightarrow> P A \<Longrightarrow> P (\<Omega> - A)"
1.45      and union: "\<And>A. disjoint_family A \<Longrightarrow> range A \<subseteq> sigma_sets \<Omega> G \<Longrightarrow> (\<And>i. P (A i)) \<Longrightarrow> P (\<Union>i::nat. A i)"
1.46    shows "P A"
1.47 -proof%unimportant -
1.48 +proof -
1.49    let ?D = "{ A \<in> sigma_sets \<Omega> G. P A }"
1.50    interpret sigma_algebra \<Omega> "sigma_sets \<Omega> G"
1.51      using closed by (rule sigma_algebra_sigma_sets)
1.52 @@ -1633,12 +1633,12 @@
1.53
1.54  subsubsection \<open>Constructing simple @{typ "'a measure"}\<close>
1.55
1.56 -lemma%important emeasure_measure_of:
1.57 +proposition emeasure_measure_of:
1.58    assumes M: "M = measure_of \<Omega> A \<mu>"
1.59    assumes ms: "A \<subseteq> Pow \<Omega>" "positive (sets M) \<mu>" "countably_additive (sets M) \<mu>"
1.60    assumes X: "X \<in> sets M"
1.61    shows "emeasure M X = \<mu> X"
1.62 -proof%unimportant -
1.63 +proof -
1.64    interpret sigma_algebra \<Omega> "sigma_sets \<Omega> A" by (rule sigma_algebra_sigma_sets) fact
1.65    have "measure_space \<Omega> (sigma_sets \<Omega> A) \<mu>"
1.66      using ms M by (simp add: measure_space_def sigma_algebra_sigma_sets)