# Zulip Chat Archive

## Stream: new members

### Topic: '' of finite set

#### Damiano Testa (Aug 20 2020 at 08:30):

Dear All,

once more, a Lean syntax question. The mwe is as follows

```
import topology.basic
def images {X Y : Type} (f : X → Y) (S : finset X) := f '' S
```

where Lean complains that `f ''`

expects a `set`

, not a `finset`

. In my actual context, it is not important that the set S is finite, so simply knowing how to convert a `finset`

to a `set`

could solve this issue. Later on, though, I will need the assumption that `S`

is finite, so ideally I would also like to be able to use this information later on.

I hope that my question is clear!

#### Johan Commelin (Aug 20 2020 at 08:33):

There is `finset.image`

#### Johan Commelin (Aug 20 2020 at 08:33):

But it doesn't have nice notation

#### Johan Commelin (Aug 20 2020 at 08:33):

Otherwise `S.to_set`

will work

#### Johan Commelin (Aug 20 2020 at 08:34):

Note that there are 2 approaches to finite sets: `set.finite`

and `finset`

.

#### Johan Commelin (Aug 20 2020 at 08:34):

There is a reasonable amount of glue between the two approaches.

#### Johan Commelin (Aug 20 2020 at 08:35):

(Also, `set.finite`

depends on `finset`

.)

#### Damiano Testa (Aug 20 2020 at 08:37):

Ok, `S.to_set`

solved the question, thanks!

The issue with `finset`

and `set.finite`

is out of my hands, since the set `S`

comes from the output of a function defined by someone else and it is a `finset`

.

#### Damiano Testa (Aug 20 2020 at 08:37):

What do I need to convert a `set`

to a `finset`

?

#### Johan Commelin (Aug 20 2020 at 08:39):

If you have `s : set X`

and `hs : s.finite`

then `hs.to_finset`

is the `finset`

that will convert back to `s`

under `finset.to_set`

.

#### Johan Commelin (Aug 20 2020 at 08:40):

"convert" means: there is a theorem. It isn't a definitional equality.

#### Damiano Testa (Aug 20 2020 at 08:41):

Ok, I will try, thanks!

Last updated: Dec 20 2023 at 11:08 UTC