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

docs#set.bind_def

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