Zulip Chat Archive

Stream: maths

Topic: set builder notation


view this post on Zulip 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}.

view this post on Zulip Chris Hughes (Jan 12 2020 at 19:33):

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

view this post on Zulip 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}

view this post on Zulip 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!

view this post on Zulip Chris Hughes (Jan 12 2020 at 20:08):

There's the definition in the first post.

view this post on Zulip 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