Apply function to every Element in a set

Stream: Is there code for X?

[Christian K]

Is it possible to apply a function to every element in a set.
A very basic example would be this function:

def add_one (x : Set ℕ) : Set ℕ := sorry

It takes a set of Natural Numbers and (should) add 1 to every element and return a new set.

[Kyle Miller]

Yes, that's docs#Set.image, which has the notation f '' s for f the function you want to apply to s.

[Christian K]

Thank you very much, I overlooked this one