# Zulip Chat Archive

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

#### King Arthur (Sep 24 2022 at 13:03):

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.

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

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