exists_finset_of...

Stream: general

[Johan Commelin]

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]

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

[Johan Commelin]

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

[Kevin Buzzard]

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

[Floris van Doorn]

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