unique

Stream: general

[Kenny Lau]

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

[Kenny Lau]

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]

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

[Patrick Massot]

What about using a product type?

[Kevin Buzzard]

Yes, exists unique does not concatenate correctly

[Mario Carneiro]

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

[Patrick Massot]

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

[Mario Carneiro]

exists_unique is the only other version

[Mario Carneiro]

there is no prop valued class like unique AFAIK

[Mario Carneiro]

you could use nonempty (unique A) of course

[Patrick Massot]

This is so ridiculous.

[Markus Himmel]

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

[Kevin Buzzard]

How about card = 1?

[Mario Carneiro]

I assume that's one of the two mentioned uses

[Markus Himmel]

It's the second one:

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