Map from one set to another

Stream: new members

[An Qi Zhang]

Hello, I was wondering if there's a way to write a function that maps from one set to another set?

For example, with Lists we have List.map, where we can provide a function to map elements in a list. For Sets, is there something similar?

Here's a MWE to help illustrate my question:

import Mathlib

namespace MWE

abbrev Nat.toString : Nat → String
| n => s!"{n}"

/- Map from Nats to Strings -/
abbrev NatsToStringsList : List Nat → List String
| ns => ns.map Nat.toString

/- How do we map from Nat to String Sets -/
abbrev NatsToStrings : Set Nat → Set String
| ns => sorry

[Etienne Marion]

Set.image?

[Andrew Yang]

If you are doing computation I would suggest to use Finset instead of Set and use docs#Finset.image

[An Qi Zhang]

Thanks! My question is then why Finset? What's the difference in using a Finset vs. Set? Does this change if I want to write lemmas or theorems?

[Kenny Lau]

@An Qi Zhang the difference is that {n : Nat | n.even } is a set and there is no way to list every element of that set, but a Finset is built with the list of the elements, so you can only compute using Finset. Yes, it changes every theorem you want to write, because Set and Finset are totally incompatible.