changeset 66827 | c94531b5007d |
parent 66703 | 61bf958fa1c1 |
child 66884 | c2128ab11f61 |
66826:0d60d2118544 | 66827:c94531b5007d |
---|---|
4 *) |
4 *) |
5 |
5 |
6 section \<open>Tagged divisions used for the Henstock-Kurzweil gauge integration\<close> |
6 section \<open>Tagged divisions used for the Henstock-Kurzweil gauge integration\<close> |
7 |
7 |
8 theory Tagged_Division |
8 theory Tagged_Division |
9 imports |
9 imports Connected |
10 Topology_Euclidean_Space |
|
11 begin |
10 begin |
12 |
11 |
13 term comm_monoid |
12 term comm_monoid |
14 |
13 |
15 lemma sum_Sigma_product: |
14 lemma sum_Sigma_product: |