Zulip Chat Archive

Stream: maths

Topic: is_singleton Prop?


Bernd Losert (Nov 29 2021 at 17:52):

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 (Nov 29 2021 at 17:57):

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

Reid Barton (Nov 29 2021 at 18:01):

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 (Nov 29 2021 at 18:02):

Yes, I'm talking about set.

Bernd Losert (Nov 29 2021 at 18:04):

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

Yaël Dillies (Nov 29 2021 at 18:15):

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

Kyle Miller (Nov 29 2021 at 18:20):

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

Bernd Losert (Nov 29 2021 at 18:28):

Ah, subsingleton is what I need actually. Thanks.


Last updated: Dec 20 2023 at 11:08 UTC