equal
deleted
inserted
replaced
6 |
6 |
7 header {* Measure spaces and their properties *} |
7 header {* Measure spaces and their properties *} |
8 |
8 |
9 theory Measure_Space |
9 theory Measure_Space |
10 imports |
10 imports |
11 Sigma_Algebra |
11 Measurable |
12 "~~/src/HOL/Multivariate_Analysis/Extended_Real_Limits" |
12 "~~/src/HOL/Multivariate_Analysis/Extended_Real_Limits" |
13 begin |
13 begin |
14 |
14 |
15 lemma sums_def2: |
15 lemma sums_def2: |
16 "f sums x \<longleftrightarrow> (\<lambda>n. (\<Sum>i\<le>n. f i)) ----> x" |
16 "f sums x \<longleftrightarrow> (\<lambda>n. (\<Sum>i\<le>n. f i)) ----> x" |