Function sets with distinct mappings

24 views

Skip to first unread message

unread,

Feb 27, 2022, 5:32:27 PM2/27/22

to tlaplus

I am trying to make a set of functions of mappings of sender->receiver:

Users == {"jack", "jill", "cindy", "bobby"}

UserSenderSet == [Users -> Users]

This almost does what I want, but we have many functions where sender->receiver are the same person, which is not what I want:

[jack |-> "jack", jill |-> "jack", cindy |-> "jack", bobby |-> "jack"]

How do I go about filtering down to set of functions that don't contain mappings of to themselves?

unread,

Feb 27, 2022, 5:51:36 PM2/27/22

to tlaplus

UserSenderSet == { f \in [Users -> Users] : \A u \in Users : f[u] /= u }

unread,

Feb 27, 2022, 6:22:26 PM2/27/22

to tlaplus

Ugh, I should have known that...thanks!

Reply all

Reply to author

Forward

0 new messages