## Stream: new members

### Topic: Defining a function

#### King Arthur (Sep 24 2022 at 12:31):

Say you have a type X and a proof that x : X can only take on n distinct cases. Is it then possible to define a function from X to some type Y using each of those cases without necessarily making X an inductive type?

#### Anne Baanen (Sep 24 2022 at 12:44):

The way to do this depends a lot on the way you prove that x : X can only take on n distinct values. For example, we have the notation ![1, 2, 3] for writing a function fin 3 → ℤ. So if you have a surjective function f : fin n → X then you can take the section of f and compose it with a function like ![...].

#### King Arthur (Sep 24 2022 at 12:57):

Good to know! But for the sake of simplicity, let's say there are only two cases: like, maybe x : X is either some object e : X or anything else that isn't e. How would I approach making f : X → Y using these two cases?

#### Anne Baanen (Sep 24 2022 at 13:02):

You can use an if expression: def f (x : X) := if h : x = e then _ else _ (see docs#ite or docs#dite)

I see, thanks!

#### King Arthur (Sep 25 2022 at 20:20):

Also, is it possible to define a function from a set of ordered pairs, given a proof that it passes the vertical line test?

#### Kevin Buzzard (Sep 25 2022 at 20:38):

Not without classical.some but yes

#### King Arthur (Sep 25 2022 at 20:48):

I'm fine with classical.some haha. is there any specific API for this task? or is this a lot more complicated than I'm thinking it is

#### Yakov Pechersky (Sep 25 2022 at 20:54):

Not complicated. What's the set you have? What if the caller of the function gives you a term that isn't in any of the pairs?

#### King Arthur (Sep 25 2022 at 21:01):

right, fair. but let's say you do also have a proof that there's a unique pair for every single object in the domain. would that be enough?

#### Yakov Pechersky (Sep 25 2022 at 21:04):

I imagine the expression of that assumption is "H : forall x : X, exists p in s, p.1 = x", then your function is "lambda x, (classical.some (H x)).2"

#### Yakov Pechersky (Sep 25 2022 at 21:04):

You don't even need a unique pair to define the function, just a pair.

oh neat, thanks!

#### Yakov Pechersky (Sep 25 2022 at 21:07):

Or you can phrase it like "H : forall x : X, exists y : Y, (x, y) in s", and the function is "lambda x, classical.some (H x)"

Last updated: Dec 20 2023 at 11:08 UTC