equal
deleted
inserted
replaced
1 (* Author: John Harrison |
1 (* Author: John Harrison |
2 Author: Robert Himmelmann, TU Muenchen (Translation from HOL light) |
2 Author: Robert Himmelmann, TU Muenchen (Translation from HOL light) |
3 Huge cleanup by LCP |
3 Huge cleanup by LCP |
4 *) |
4 *) |
5 |
5 |
6 section \<open>Henstock-Kurzweil gauge integration in many dimensions\<close> |
6 section \<open>Henstock-Kurzweil Gauge Integration in Many Dimensions\<close> |
7 |
7 |
8 theory Henstock_Kurzweil_Integration |
8 theory Henstock_Kurzweil_Integration |
9 imports |
9 imports |
10 Lebesgue_Measure Tagged_Division |
10 Lebesgue_Measure |
|
11 Tagged_Division |
11 begin |
12 begin |
12 |
13 |
13 lemma norm_diff2: "\<lbrakk>y = y1 + y2; x = x1 + x2; e = e1 + e2; norm(y1 - x1) \<le> e1; norm(y2 - x2) \<le> e2\<rbrakk> |
14 lemma norm_diff2: "\<lbrakk>y = y1 + y2; x = x1 + x2; e = e1 + e2; norm(y1 - x1) \<le> e1; norm(y2 - x2) \<le> e2\<rbrakk> |
14 \<Longrightarrow> norm(y-x) \<le> e" |
15 \<Longrightarrow> norm(y-x) \<le> e" |
15 using norm_triangle_mono [of "y1 - x1" "e1" "y2 - x2" "e2"] |
16 using norm_triangle_mono [of "y1 - x1" "e1" "y2 - x2" "e2"] |