is_singleton Prop?

Stream: maths

[Bernd Losert]

Is there an is_singleton Prop in mathlib such that is_singleton s means that s is a singleton set (has only one element)? I couldn't find one in the docs.

[Alex J. Best]

Are you asking about the set type? Or finset, or about how to express that a type has one element?

[Reid Barton]

Related: https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there.20code.20for.20X.3F/topic/Prop-valued.20.22I.20have.20one.20term.22/near/260587918

[Bernd Losert]

Yes, I'm talking about set.

[Bernd Losert]

So right now, I'm doing x ∈ s → s = {x}. That seems to work.

[Yaël Dillies]

This doesn't describe a singleton set but a subsingleton (the empty set respects it). See docs#set.subsingleton.

[Kyle Miller]

This is how I've written it before: ∃ x, s = {x}

[Bernd Losert]

Ah, subsingleton is what I need actually. Thanks.