Defining a function to a subset of the codomain

Question

I am trying to define the image restriction of a function
f : A → B as f': A → f[A], where f'(a) = f(a) . However, I am not sure how to define it in a lean.
In my opinion, the most intuitive way to define it is:

def fun_to_image {A B: Type*} (f: A → B): A → image f set.univ :=
        λ a, f a

However, this gets rejected because (f a) is of type B not (image f set.univ).

I even tried proving that f(a) ∈ (image f univ) . It didn't help:

def fun_to_image (f : A → B) : A → image f univ := 
    λ a , 
    have h : f a ∈ image f univ := 
        exists.intro a 
            (and.intro trivial (eq.refl (f a))),
    f a

The error message is:

type mismatch, term
  λ (a : A), f a
has type
  A → B
but is expected to have type
  A → ↥(f '' univ)

set.univ and image are defined as follows in data.set

def univ : set α :=
λ a, true

def image (f : α → β) (s : set α) : set β :=
{b | ∃ a, a ∈ s ∧ f a = b}

Any idea how this can be done?

Answer 1

You are almost there (-;

There is a little “warning sign” in the error message.

but is expected to have type
  A → ↥(f '' univ)

You can see the creepy up-arrow ↥. Let me explain what it means:

As you have recalled, image f set.univ is defined as a subset. Since you are treating it as a type, it is automatically coerced into a so-called subtype: if s : set X, then the corresponding subtype s has terms of the form ⟨x, h⟩ (type these as \< and \> in VScode), where x : X and h : x ∈ s.

This “coercion to type” is indicated by the ↥.

So, to finish your definition, you will have to write ⟨f a, h⟩, instead of f a.

---

Note that in main library there is also a definition of range (here) which is meant to be used in place of image _ set.univ. It already comes with (L1167)

def range_factorization (f : ι → β) : ι → range f :=
λ i, ⟨f i, mem_range_self i⟩