equal
deleted
inserted
replaced
4187 "d division_of (cbox a b) \<Longrightarrow> setsum content d = content (cbox a b)" |
4187 "d division_of (cbox a b) \<Longrightarrow> setsum content d = content (cbox a b)" |
4188 by (metis division_ofD(1) monoidal_monoid operative_content operative_division setsum_iterate) |
4188 by (metis division_ofD(1) monoidal_monoid operative_content operative_division setsum_iterate) |
4189 |
4189 |
4190 lemma additive_content_tagged_division: |
4190 lemma additive_content_tagged_division: |
4191 "d tagged_division_of (cbox a b) \<Longrightarrow> setsum (\<lambda>(x,l). content l) d = content (cbox a b)" |
4191 "d tagged_division_of (cbox a b) \<Longrightarrow> setsum (\<lambda>(x,l). content l) d = content (cbox a b)" |
4192 unfolding operative_tagged_division[OF monoidal_monoid operative_content assms,symmetric] |
4192 unfolding operative_tagged_division[OF monoidal_monoid operative_content,symmetric] |
4193 using setsum_iterate by blast |
4193 using setsum_iterate by blast |
4194 |
4194 |
4195 |
4195 |
4196 subsection \<open>Finally, the integral of a constant\<close> |
4196 subsection \<open>Finally, the integral of a constant\<close> |
4197 |
4197 |