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