## Stream: Is there code for X?

### Topic: set.finite.of_surjective

#### Adam Topaz (Apr 05 2021 at 21:56):

Do we have a lemma saying that a set S : set X is finite given there is a function f : Y \to X and a finite set T : set Y such that every element of S is the image of some element of T?

#### Greg Price (Apr 05 2021 at 22:00):

Could you use set.finite.image and set.finite.subset?

#### Adam Topaz (Apr 05 2021 at 22:01):

Thanks, set.finite.image should do

Last updated: May 17 2021 at 16:26 UTC