Notation for sets parametrized

Stream: Is there code for X?

[Miguel Marco]

Say i want to construct the set of squares of the elements of a set S. AFAIK, there are two natural ways to denote this:

def M := {n : ℕ | ∃ p ∈ S ∧ n = p ^ 2}

or to define a function that squares the elements, and then take the image

def f : ℕ → ℕ := λ x, x^2
def M := f '' S

but in math books and papers, we would just use

{x^2 | x ∈ S}

Is there a way to use similar notation in Lean? Or could it be defined somehow?

[Kyle Miller]

I think in Lean 3 the syntax is {(x^2) | (x ∈ S)}, but I tend to forget off the top of my head. After the | you can have a list of function-argument-like binders, just like in lambda/def notation

There's also set.image notation paired with lambda notation, without using an intermediate definition: (λ x, x^2) '' S

[Eric Wieser]

Usually the '' spelling is preferred because we have lemmas about it