Zulip Chat Archive

Stream: general

Topic: new set notations


Patrick Massot (Aug 19 2020 at 12:18):

I'm a bit disappointed that the new set notation doesn't seem to be defeq to set.image:

import data.set.basic

open set

example (f :   ) (s : set ) (h : 1  s) : f 1  f '' s :=
mem_image_of_mem f h

example (f :   ) (s : set ) (h : 1  s) : f 1  {(f x) | x  s} :=
mem_image_of_mem f h -- doesn't work

Is this something that could be fixed? Or should we duplicate the whole set.image API?

Johan Commelin (Aug 19 2020 at 12:24):

Maybe it's time to redefine image?

Mario Carneiro (Aug 19 2020 at 18:38):

I think you should just live with the difference. The new notation also gives something different when you use more binders, i.e. {(f x y) | x y ∈ s} doesn't express anything that can be defined in terms of image or the 1D notation, so if we try to make a library around the notation version our work would never be done

Mario Carneiro (Aug 19 2020 at 18:40):

We could have a tactic (a simp proc - gasp!) to rewrite the new notation into an appropriate application of image

Yury G. Kudryashov (Aug 20 2020 at 04:59):

{(f x y) | x y ∈ s} is very similar to docs#set.image2

Yury G. Kudryashov (Aug 20 2020 at 04:59):

BTW, Lean doesn't use new notation for pretty-printing.


Last updated: Dec 20 2023 at 11:08 UTC