Zulip Chat Archive

Stream: Is there code for X?

Topic: Function Property for `rel`


view this post on Zulip Marcus Rossel (Dec 29 2020 at 19:57):

Is there a definition of the "function"-property of a relation, in the sense of : "it associates every instance of the first type to exactly one instance of the second type"?
And if so, is there a method for turning a rel α β into α → β?

view this post on Zulip Yury G. Kudryashov (Dec 31 2020 at 20:22):

We have docs#relator.right_unique and docs#relator.left_total

view this post on Zulip Yury G. Kudryashov (Dec 31 2020 at 20:22):

(BTW, they should be made non-classes because we have 0 instances)

view this post on Zulip Yury G. Kudryashov (Dec 31 2020 at 21:07):

You can use docs#classical.some to get f : α → β from ∀ x, ∃ y, r x y.


Last updated: May 16 2021 at 05:21 UTC