Where can I find in Isabelle the construction that takes a family of sets as input and outputs the disjoint union of this family?
Theory Sum does that but only for a family of two.
Larry told me there is
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: Sep 25 2022 at 22:23 UTC