Zulip Chat Archive

Stream: maths

Topic: why `nonempty`?


view this post on Zulip Kevin Buzzard (Feb 16 2020 at 11:16):

So the community seems to have decided that the best way to express the predicate "I am non-empty" on a term of type set X is via dot notation, i.e. defining the predicate set.nonempty. Is it just true in general that any predicate P on set X should just be called set.P and should always be dealt with that way, and we can just let the notationiser fix this up, because it looks weird for mathematicians? [For linguistic reasons unrelated to computers, we mathematicians adopted the notation XX\not=\emptyset, perhaps because it allows us to write "For every XS,\emptyset\not=X\in S,\ldots"?

view this post on Zulip Kevin Buzzard (Feb 16 2020 at 11:17):

Also, which predicates should be classes?

view this post on Zulip Kevin Buzzard (Feb 16 2020 at 11:36):

I also think that current mathematical usage of ABA\cong B corresponds to something like Lean's nonempty (A ≅ B) -- ours is a predicate. And what are all those →ₐ things? They're all just \to.

view this post on Zulip Mario Carneiro (Feb 16 2020 at 12:04):

I think the reason it is called set.nonempty is simply because nonempty already exists and means something else

view this post on Zulip Mario Carneiro (Feb 16 2020 at 12:05):

I would say it is similar to nat.succ; you don't have to use dot notation for it, it's just in the namespace, but you can if you want

view this post on Zulip Kevin Buzzard (Feb 16 2020 at 12:36):

We don't mind you using it, we just want it to be hidden from us by the notationizer.

view this post on Zulip Kevin Buzzard (Feb 16 2020 at 12:38):

Presumably nonempty is in the root namespace because it is actually Sort.nonempty


Last updated: May 18 2021 at 07:19 UTC