evaluation map from sets to sets

Stream: Is there code for X?

[Xavier Xarles]

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]

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]

I don't think this is in mathlib yet.

[Xavier Xarles]

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]

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

[Xavier Xarles]

nice, it works, thank you

[Adam Topaz]

@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]

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]

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]

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]

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]

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]

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]

Yeah, pure a for the monad set is the singleton {a}, and bind is given by a big union.

[Adam Topaz]

docs#set.bind_def

[Kyle Miller]

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 ($)?