Zulip Chat Archive

Stream: general

Topic: Notation for univ

Yaël Dillies (Aug 19 2022 at 19:38):

We have no notation for set.univ and finset.univ. What do people think of introducing Ω as such a notation? That would an alternative to using it as the base type in probability theory.
cc @Jason KY.

Jason KY. (Aug 19 2022 at 19:47):

I think the decision to use of Ω : Type* in probability theory was very popular and I do use set.univ quite often when working with probability so I don't support using Ω for set.univ. It would be useful to have a notation for set.univhowever.

Junyan Xu (Aug 19 2022 at 19:52):

Is not a notation?

Yaël Dillies (Aug 19 2022 at 19:53):

It's notation for docs#has_top.top

Eric Rodriguez (Aug 19 2022 at 19:56):

but that is defeq right?

Yaël Dillies (Aug 19 2022 at 19:57):

But not syntactically equal! So that will mess with rw.

Yaël Dillies (Aug 19 2022 at 19:57):

So is notation for something that's defeq to univ, but that doesn't make it notation for univ.

Eric Rodriguez (Aug 19 2022 at 19:59):

a notation typeclass will have the same issue, and I'm not sure how you could make notation overriding work here unless you had a different one for finset/set

Eric Rodriguez (Aug 19 2022 at 19:59):

i guess this comes back to the age-old "we don't want mathematicians to have to use lattices" and stuff like that

Thomas Browning (Aug 19 2022 at 19:59):

Would redefining set.univ to help?

Yaël Dillies (Aug 19 2022 at 20:00):

Maybe! I just don't want to be murdered by a mob of angry mathematicians.

Patrick Massot (Aug 19 2022 at 20:51):

I always love notations when they allow to bring Lean code closer to real world math. But set.univdoesn't exist in the real world (or you could say that X is notation for (set.univ : set X)) so I don't think a notation would help here.

Johan Commelin (Aug 20 2022 at 17:17):

Exactly for the reason that Patrick says, I wouldn't really mind writing everywhere. I think that for a random mathematician has about the same clarity as univ.

Eric Rodriguez (Aug 20 2022 at 17:37):

but we still preserve emptyc, right?

Wrenna Robson (Aug 22 2022 at 11:19):

Yeah, I have to say unless you are getting rid of emptyc I don't think this is a good idea.

Wrenna Robson (Aug 22 2022 at 11:22):

Do we use ℧ for anything?

Wrenna Robson (Aug 22 2022 at 11:22):

It has the advantage of looking a bit like a weird U

Wrenna Robson (Aug 22 2022 at 11:22):

but is also upside-down Ω so it has that association.

Wrenna Robson (Aug 22 2022 at 11:24):

Conceptually, I think the reason I don't like the top/bottom symbols is that while there is a natural lattice on sets, somehow the definition of sets doesn't rest on that - the empty and universal sets are defined before the lattice.

Wrenna Robson (Aug 22 2022 at 11:25):

Also, there might be contexts where you have a lattice of sets and you want to talk about the top of that lattice as opposed to the universal set.

Eric Rodriguez (Aug 22 2022 at 11:28):

the definition is already there, and you can already get goals of the form \top = coe \top today.

Wrenna Robson (Aug 22 2022 at 13:32):

True, true.

Violeta Hernández (Jan 19 2023 at 23:39):

I like . I don't want yet another vs Ø vs 0 situation :stuck_out_tongue:

Last updated: Dec 20 2023 at 11:08 UTC