# Zulip Chat Archive

## Stream: maths

### Topic: set builder notation

#### Enrico Borba (Jan 12 2020 at 19:31):

Where is the `notation`

declaration for set builder notation in the lean source? I'm trying to understand what exactly I can put before the `|`

in `{ x | even x }`

. Is it only a _single identifier_ that I can place there, so it just becomes a `λ x, even x`

? The main reason I'm asking is because I was hoping to do something like `{(a, f a) | a ∈ A}`

. But I've currently resorted to `{x : A × B | f x.1 = x.2}`

.

#### Chris Hughes (Jan 12 2020 at 19:33):

You do have to do it the ugly way I'm afraid.

#### Chris Hughes (Jan 12 2020 at 19:36):

There might be good notation for this in Lean 4. But the main downside would be that I expect it would end up having to unfold to something like `{x : A × B | ∃ a : A, (a, f a) = x}`

#### Kevin Buzzard (Jan 12 2020 at 20:07):

I think it has to unfold to something like this because that's the only definition I can think of for the set!

#### Chris Hughes (Jan 12 2020 at 20:08):

There's the definition in the first post.

#### Patrick Massot (Jan 12 2020 at 20:14):

The set builder notation of Lean is of a really different nature as what Enrico wants. It is purely syntactic sugar for defining sets (in the sense of type theory, so all elements have the same type `X`

and a set is a map from `X`

to `Prop`

). Writing `{(a, f(a)) | a ∈ A}`

is the image of a set `A`

under a function, it involves an existential quantifier. Actually I'm not even sure what is meant because `A`

seems to be a set or a type depending on the sentence.

Last updated: May 10 2021 at 07:15 UTC