nonempty sets

Stream: maths

[Yury G. Kudryashov]

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?

[Kenny Lau]

context?

[Yury G. Kudryashov]

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.

[Kenny Lau]

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

[Yury G. Kudryashov]

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

[Kenny Lau]

I don't know

[Kevin Buzzard]

These are important questions in some contexts I guess

[Yury G. Kudryashov]

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