# Zulip Chat Archive

## Stream: maths

### Topic: why `nonempty`?

#### 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 $X\not=\emptyset$, perhaps because it allows us to write "For every $\emptyset\not=X\in S,\ldots$"?

#### Kevin Buzzard (Feb 16 2020 at 11:17):

Also, which predicates should be classes?

#### Kevin Buzzard (Feb 16 2020 at 11:36):

I also think that current mathematical usage of $A\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$.

#### 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

#### 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

#### 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.

#### 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