box integrals: `ι` or `fin n`

Stream: maths

[Yury G. Kudryashov]

When I define box integrals, I use ι → ℝ in most of the files. Now I think that may be I should only deal with ι = fin n. Formally, it is less general but we are not going to use these integrals in real-world applications (other than the divergence theorem which is formulated only for fin (n + 1) → ℝ).

[Johan Commelin]

So you are saying this basically only part of API development? In that case: do whatever you want. The final theorems should probably be done for ι → ℝ though.

[Yury G. Kudryashov]

The divergence theorem uses docs#fin.insert_nth

[Yury G. Kudryashov]

I tried to do it with subtypes instead but it looks worse.

[Yury G. Kudryashov]

And the divergence theorem is probably the only result about gauge integrals that we use outside of analysis.box_integral.

[Yury G. Kudryashov]

(one more: a Bochner integrable function is McShane and Henstock integrable with the same integral)