# Zulip Chat Archive

## Stream: general

### Topic: new set notations

#### Patrick Massot (Aug 19 2020 at 12:18):

I'm a bit disappointed that the new set notation doesn't seem to be defeq to `set.image`

:

```
import data.set.basic
open set
example (f : ℕ → ℕ) (s : set ℕ) (h : 1 ∈ s) : f 1 ∈ f '' s :=
mem_image_of_mem f h
example (f : ℕ → ℕ) (s : set ℕ) (h : 1 ∈ s) : f 1 ∈ {(f x) | x ∈ s} :=
mem_image_of_mem f h -- doesn't work
```

Is this something that could be fixed? Or should we duplicate the whole `set.image`

API?

#### Johan Commelin (Aug 19 2020 at 12:24):

Maybe it's time to redefine `image`

?

#### Mario Carneiro (Aug 19 2020 at 18:38):

I think you should just live with the difference. The new notation also gives something different when you use more binders, i.e. `{(f x y) | x y ∈ s}`

doesn't express anything that can be defined in terms of `image`

or the 1D notation, so if we try to make a library around the notation version our work would never be done

#### Mario Carneiro (Aug 19 2020 at 18:40):

We could have a tactic (a simp proc - gasp!) to rewrite the new notation into an appropriate application of `image`

#### Yury G. Kudryashov (Aug 20 2020 at 04:59):

`{(f x y) | x y ∈ s}`

is very similar to docs#set.image2

#### Yury G. Kudryashov (Aug 20 2020 at 04:59):

BTW, Lean doesn't use new notation for pretty-printing.

Last updated: May 10 2021 at 19:16 UTC