'' of finite set

Stream: new members

[Damiano Testa]

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]

There is finset.image

[Johan Commelin]

But it doesn't have nice notation

[Johan Commelin]

Otherwise S.to_set will work

[Johan Commelin]

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

[Johan Commelin]

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

[Johan Commelin]

(Also, set.finite depends on finset.)

[Damiano Testa]

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]

What do I need to convert a set to a finset?

[Johan Commelin]

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]

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

[Damiano Testa]

Ok, I will try, thanks!