set.finite.of_surjective

Stream: Is there code for X?

[Adam Topaz]

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]

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

[Adam Topaz]

Thanks, set.finite.image should do