equal
deleted
inserted
replaced
5 *) |
5 *) |
6 |
6 |
7 section \<open>The area of a circle\<close> |
7 section \<open>The area of a circle\<close> |
8 |
8 |
9 theory Circle_Area |
9 theory Circle_Area |
10 imports Complex_Main Interval_Integral |
10 imports Complex_Main "HOL-Analysis.Interval_Integral" |
11 begin |
11 begin |
12 |
12 |
13 lemma plus_emeasure': |
13 lemma plus_emeasure': |
14 assumes "A \<in> sets M" "B \<in> sets M" "A \<inter> B \<in> null_sets M" |
14 assumes "A \<in> sets M" "B \<in> sets M" "A \<inter> B \<in> null_sets M" |
15 shows "emeasure M A + emeasure M B = emeasure M (A \<union> B)" |
15 shows "emeasure M A + emeasure M B = emeasure M (A \<union> B)" |