Where can I find in Isabelle the construction that takes a family of sets as input and outputs the disjoint union of this family?

`Sum`

in `Theory Sum`

does that but only for a family of two.

Larry told me there is `Sigma`

in `Product_Type.thy`

for this purpose.

Indeed there is, I use it often. It's very useful also in combination with the summation operator.

Last updated: Aug 13 2022 at 06:26 UTC