## Stream: Is there code for X?

### Topic: Function Property for rel

#### 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 α → β?

#### Yury G. Kudryashov (Dec 31 2020 at 20:22):

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

#### 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