Zulip Chat Archive

Stream: general

Topic: exists_finset_of...


view this post on Zulip Johan Commelin (May 08 2019 at 12:18):

I wrote the following file for the perfectoid project: https://github.com/leanprover-community/lean-perfectoid-spaces/blob/master/src/for_mathlib/finset.lean
Main result:

lemma exists_finset_of_subset_image (s : set α) (h : (t : set β)  f '' s) :
 (s' : finset α), s'.image f = t  (s' : set α)  s :=

Is this file suitable for mathlib? Should it be rewritten in a different way? I still feel uneasy around finsets...

view this post on Zulip Johan Commelin (May 08 2019 at 12:23):

Ooh, lololol... I just found subset_image_iff in finset.lean.

view this post on Zulip Johan Commelin (May 08 2019 at 12:23):

Never mind... we can just delete this file then (-;

view this post on Zulip Kevin Buzzard (May 08 2019 at 13:57):

That's the best kind of progress :D We have 6000 lines pencilled in "for mathlib" so still plenty to go :-/

view this post on Zulip Floris van Doorn (May 08 2019 at 20:40):

Yes, I added this to mathlib a little while ago :)


Last updated: May 12 2021 at 04:19 UTC