Hi The Anh, if you want to construct the set of the elements (i.e., the co-domain) of a sequence you can define Range(s) == { s[i] : i \in DOMAIN s } Of course, you lose the information on the order and the multiplicity of the elements in the original sequence. Hope this helps, Stephan
--
You received this message because you are subscribed to the Google Groups "tlaplus" group. To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx. To post to this group, send email to tlaplus@xxxxxxxxxxxxxxxx. Visit this group at https://groups.google.com/group/tlaplus. To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/0585E81D-7EFD-4FC4-9E57-6EDCA6D70F19%40gmail.com. For more options, visit https://groups.google.com/d/optout. |