Set from finset is finite

Stream: Is there code for X?

[Marcus Rossel]

Is there a lemma proving roughly that sets constructed from finsets are finite?

example {α β : Type*} (s : finset β) (f : α → β) (h : function.injective f) : { x | f x ∈ s }.finite

[Yakov Pechersky]

We don't have finset.comap, hmm.

[Yakov Pechersky]

Ah, docs#finset.preimage

[Yakov Pechersky]

and docs#set.finite.preimage

[Yakov Pechersky]

The proof (term mode!) is pretty much exactly the statement, thanks to projection notation:

import data.set.finite

example {α β : Type*} (s : finset β) (f : α → β) (h : function.injective f) :
  { x | f x ∈ s }.finite :=
s.finite_to_set.preimage (h.inj_on _)