equal
deleted
inserted
replaced
3 Author: Robert Himmelmann, TU München |
3 Author: Robert Himmelmann, TU München |
4 Author: Jeremy Avigad |
4 Author: Jeremy Avigad |
5 Author: Luke Serafin |
5 Author: Luke Serafin |
6 *) |
6 *) |
7 |
7 |
8 section \<open>Lebesgue measure\<close> |
8 section \<open>Lebesgue Measure\<close> |
9 |
9 |
10 theory Lebesgue_Measure |
10 theory Lebesgue_Measure |
11 imports Finite_Product_Measure Bochner_Integration Caratheodory Complete_Measure Summation_Tests Regularity |
11 imports |
|
12 Finite_Product_Measure |
|
13 Caratheodory |
|
14 Complete_Measure |
|
15 Summation_Tests |
|
16 Regularity |
12 begin |
17 begin |
13 |
18 |
14 lemma measure_eqI_lessThan: |
19 lemma measure_eqI_lessThan: |
15 fixes M N :: "real measure" |
20 fixes M N :: "real measure" |
16 assumes sets: "sets M = sets borel" "sets N = sets borel" |
21 assumes sets: "sets M = sets borel" "sets N = sets borel" |