Stream: Beginner Questions

Topic: disjoint union of sets

Anthony Bordg (Dec 12 2020 at 11:30):

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.

Anthony Bordg (Dec 13 2020 at 13:58):

Larry told me there is Sigma in Product_Type.thy for this purpose.

Manuel Eberl (Dec 13 2020 at 15:33):

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

Last updated: Nov 13 2025 at 04:27 UTC