## Stream: general

### Topic: unique

#### Kenny Lau (Jun 27 2020 at 09:31):

how do I write "there are a unique integer and a unique natural number such that ..."?

#### Kenny Lau (Jun 27 2020 at 09:31):

I don't think ∃! (a : \Z) (b : \N) is what I want because it says "there is a unique integer such that there is a unique natural number such that"

#### Kenny Lau (Jun 27 2020 at 09:32):

I guess I just can't write it and have to separate it into two theorems

#### Patrick Massot (Jun 27 2020 at 09:33):

What about using a product type?

#### Kevin Buzzard (Jun 27 2020 at 09:48):

Yes, exists unique does not concatenate correctly

#### Mario Carneiro (Jun 27 2020 at 09:56):

You can also use unique (\Sigma ...) etc

#### Patrick Massot (Aug 03 2020 at 15:22):

I forgot, what is the Prop-valued version of unique?

#### Mario Carneiro (Aug 03 2020 at 15:29):

exists_unique is the only other version

#### Mario Carneiro (Aug 03 2020 at 15:29):

there is no prop valued class like unique AFAIK

#### Mario Carneiro (Aug 03 2020 at 15:30):

you could use nonempty (unique A) of course

#### Patrick Massot (Aug 03 2020 at 15:30):

This is so ridiculous.

#### Markus Himmel (Aug 03 2020 at 15:30):

nonempty (unique α) and subsingleton α ∧ nonempty α are both used exactly once in mathlib

#### Mario Carneiro (Aug 03 2020 at 15:32):

I assume that's one of the two mentioned uses

#### Markus Himmel (Aug 03 2020 at 15:32):

It's the second one:

lemma eq_one_iff_subsingleton_and_nonempty {α : Type*} :
mk α = 1 ↔ (subsingleton α ∧ nonempty α)


Last updated: May 12 2021 at 05:19 UTC