Zulip Chat Archive

Stream: maths

Topic: nonempty sets


view this post on Zulip Yury G. Kudryashov (Nov 09 2019 at 02:38):

Hello, I see at least three ways to say that s : set α is not empty: nonempty s, s ≠ ∅, ∃ x, x ∈ s. Are there any "official" preferences?

view this post on Zulip Kenny Lau (Nov 09 2019 at 02:47):

context?

view this post on Zulip Yury G. Kudryashov (Nov 09 2019 at 02:58):

E.g., I see s ≠ ∅ in conditionally_complete_lattice and ∃ x, x ∈ s in data/real/basic. They're used in similar contexts: exists_sup in real/basic is very similar to le_cSup and cSup_le.

view this post on Zulip Kenny Lau (Nov 09 2019 at 03:31):

I might use {x} (hx : x \in s)

view this post on Zulip Yury G. Kudryashov (Nov 09 2019 at 03:34):

This is one more way to write the same thing. Do I understand correctly that there is no "officially" preferred way to write this?

view this post on Zulip Kenny Lau (Nov 09 2019 at 03:35):

I don't know

view this post on Zulip Kevin Buzzard (Nov 09 2019 at 07:17):

These are important questions in some contexts I guess

view this post on Zulip Yury G. Kudryashov (Nov 09 2019 at 07:42):

@Kevin Buzzard It's not convenient to have several different ways to write down the same fact used in two related files. You have to convert from one to another.


Last updated: May 06 2021 at 19:30 UTC