set builder notation

Stream: maths

[Enrico Borba]

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]

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

[Chris Hughes]

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]

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]

There's the definition in the first post.

[Patrick Massot]

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.