finsetology

Stream: general

[Johan Commelin]

Are things like

variables {α : Type*} {β : Type*} (t : finset β) (f : α → β)

lemma exists_subset_preimage (h : (↑t : set β) ⊆ range f) : ∃ (s : finset α), s.image f = t :=

hidden somewhere in the library? I couldn't find them...

[Johan Commelin]

Whoops, missing the assumption that t ⊆ range f fixed

[Floris van Doorn]

I don't think so. A very similar lemma is proved here:
https://github.com/flypitch/flypitch/blob/master/src/to_mathlib.lean#L536

lemma exists_of_subset_image {f : α → β} {s : finset β} {t : set α} (h : ↑s ⊆ f '' t) :
  ∃s' : finset α, ↑s' ⊆ t ∧ s'.image f = s

You get your lemma if you rewrite image univ to range.