Stream: Beginner Questions

Topic: disjoint union of sets


view this post on Zulip 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.

view this post on Zulip Anthony Bordg (Dec 13 2020 at 13:58):

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

view this post on Zulip 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: Sep 25 2022 at 22:23 UTC