Added some more operators

[mryndzionek]

Not sure if Range should be there, but might moved later. Some discussion already in #20.

[muenchnerkindl]

You are right. Personally, I still find the definition using the choice function easier to understand. (If you don't want to export that operator in the module, you can introduce it in a LET.)

On 28 Oct 2020, at 04:21, mryndzionek notifications@github.com wrote:

@mryndzionek commented on this pull request.

In modules/FiniteSetsExt.tla https://github.com/tlaplus/CommunityModules/pull/21#discussion_r513156489:

() ( Compute all sets that contain one element from each of the input sets: ) -( Shuffle({{1,2}, {3,4}, {5}}) = {{1,3,5}, {1,4,5}, {2,3,5}, {2,4,5}} ) +( ) +( Example: ) +( Shuffle({{1,2}, {3,4}, {5}}) = ) +( {{1,3,5}, {1,4,5}, {2,3,5}, {2,4,5}} ) () Shuffle(Sets) == { Range(f) : f \in Choice(Sets) } Shouldn't Cardinality(subsets) = Cardinality(S) be changed to Cardinality(subsets) <= Cardinality(S)? Only then this new definition is equivalent to the old one:

DifferentOneOfEach(S) == { subsets \in SUBSET (UNION S) : /\ Cardinality(subsets) <= Cardinality(S) * Cover every set in S. /\ \A s \in S: \E e \in subsets: e \in s } — You are receiving this because you commented. Reply to this email directly, view it on GitHub https://github.com/tlaplus/CommunityModules/pull/21#discussion_r513156489, or unsubscribe https://github.com/notifications/unsubscribe-auth/ABZCW5JBQDV7BWUZAGWZGWLSM6E5HANCNFSM4S5OJ73A.

[lemmy]

How about introducing ChoiceFunction in a LET as suggested by Stephan and calling the real operator simply Choices (as suggested elsewhere)?

[mryndzionek]

How about introducing ChoiceFunction in a LET as suggested by Stephan and calling the real operator simply Choices (as suggested elsewhere)?

So just adding:

Choices(Sets) == LET ChoiceFunction(Ts) == { f \in [Ts -> UNION Ts] : 
                                               \A T \in Ts : f[T] \in T }
                 IN  { Range(f) : f \in ChoiceFunction(Sets) }

?

[lemmy]

Thanks!