# Zulip Chat Archive

## Stream: Is there code for X?

### Topic: evaluation map from sets to sets

#### Xavier Xarles (Feb 03 2021 at 12:41):

Dear all,

I need to define something quite easy like

`def foo (A : Type*)(B : Type*) : A → set(A → B)→ set B `

where it send `(a:A)`

and a set `s : set(A → B)`

the set " { f(a) for f in s}". It is already defined something like this, or can somebody help me with the code?

#### Johan Commelin (Feb 03 2021 at 12:44):

You can either define it explicitly as `{x | \exists a : A, \exists f \in s, x = f a}`

.

Another option is to define it as the union of the ranges of the `f \in s`

:

```
\bigcup f \in s, set.range f
```

#### Johan Commelin (Feb 03 2021 at 12:44):

I don't think this is in mathlib yet.

#### Xavier Xarles (Feb 03 2021 at 13:07):

So the first solution will be to write something like

`def foo (A : Type*)(B : Type*) : A → set(A → B)→ set B := λ a s, {x | ∃ a : A, ∃ f ∈ s, x = f a}`

but it gives me an strange error, complaining about the f.

#### Johan Commelin (Feb 03 2021 at 13:11):

What happens if you write `\exists (f : A \to B) (h : f \in s), x = f a`

?

#### Xavier Xarles (Feb 03 2021 at 13:16):

nice, it works, thank you

#### Adam Topaz (Feb 03 2021 at 14:47):

@Xavier Xarles You can also use `do`

notation, as follows:

```
import data.set
def foo (A : Type*)(B : Type*) : A → set(A → B)→ set B := λ a fs, do {f ← fs, return (f a)}
```

I think this is quite intuitive.

#### Floris van Doorn (Feb 03 2021 at 19:09):

There are a lot of set operations that are really applications of `set.image`

and `set.preimage`

. I recommend using those, so that you can use all the properties about them. In this case, you can use:

```
import data.set.basic
def foo (A B : Type*) : A → set (A → B) → set B :=
λ x s, (λ f : A → B, f x) '' s
```

#### Floris van Doorn (Feb 03 2021 at 19:10):

A lot of properties about `set.image`

(notation `''`

) are here: https://leanprover-community.github.io/mathlib_docs/data/set/basic.html#set.mem_image_iff_bex

#### Johan Commelin (Feb 03 2021 at 19:13):

Whoops... @Xavier Xarles I now realise that my answers are maths-incorrect. You have a fixed `a`

, whereas I gave answers that range over all `a`

.

#### Adam Topaz (Feb 03 2021 at 19:19):

Just in case it helps:

```
import data.set
@[simp]
def foo {A B : Type*} : A → set (A → B) → set B := λ x s, (λ f : A → B, f x) '' s
@[simp]
def bar {A B : Type*} : A → set (A → B) → set B := λ a fs, do {f ← fs, return (f a)}
example {A B : Type*} (a : A) (fs : set (A → B)) : foo a fs = bar a fs := by tidy
```

#### Floris van Doorn (Feb 03 2021 at 19:20):

Also, `(λ f : A → B, f x)`

is `function.eval x`

, and there are already a *few* properties about images of `function.eval`

in the file I linked, like docs#set.eval_image_pi.

#### Kyle Miller (Feb 03 2021 at 22:24):

This can also be done with applicative functors rather than the full monad:

```
def foo (A : Type*) (B : Type*) : A → set (A → B) → set B := λ a fs, fs <*> pure a
```

Unfolding some definitions, it turns out that `set.seq`

applies a set of functions to a set of values and forms the set of all values:

```
def foo (A : Type*) (B : Type*) : A → set (A → B) → set B := λ a fs, fs.seq {a}
```

#### Adam Topaz (Feb 03 2021 at 22:32):

Yeah, `pure a`

for the monad `set`

is the singleton `{a}`

, and bind is given by a big union.

#### Adam Topaz (Feb 03 2021 at 22:33):

#### Kyle Miller (Feb 03 2021 at 23:07):

I should have looked at your first example more closely -- it only uses that `set`

is a functor. Point-free style using `set.image`

, which is `set`

's `functor.map`

:

```
def foo (A : Type*) (B : Type*) : A → set (A → B) → set B := set.image ∘ function.eval
```

The generalized version:

```
def foo (F) [functor F] (A : Type*) (B : Type*) : A → F (A → B) → F B := functor.map ∘ function.eval
```

I found a Haskell library where they call this function `flap`

, which is maybe a play on how `function.eval`

is equivalently `flip ($)`

?

Last updated: May 07 2021 at 22:14 UTC