Stream: general

Topic: exists_finset_of...

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...

Johan Commelin (May 08 2019 at 12:23):

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

Johan Commelin (May 08 2019 at 12:23):

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

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 :-/

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