Zulip Chat Archive

Stream: general

Topic: unique


view this post on Zulip Kenny Lau (Jun 27 2020 at 09:31):

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

view this post on Zulip 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"

view this post on Zulip Kenny Lau (Jun 27 2020 at 09:32):

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

view this post on Zulip Patrick Massot (Jun 27 2020 at 09:33):

What about using a product type?

view this post on Zulip Kevin Buzzard (Jun 27 2020 at 09:48):

Yes, exists unique does not concatenate correctly

view this post on Zulip Mario Carneiro (Jun 27 2020 at 09:56):

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

view this post on Zulip Patrick Massot (Aug 03 2020 at 15:22):

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

view this post on Zulip Mario Carneiro (Aug 03 2020 at 15:29):

exists_unique is the only other version

view this post on Zulip Mario Carneiro (Aug 03 2020 at 15:29):

there is no prop valued class like unique AFAIK

view this post on Zulip Mario Carneiro (Aug 03 2020 at 15:30):

you could use nonempty (unique A) of course

view this post on Zulip Patrick Massot (Aug 03 2020 at 15:30):

This is so ridiculous.

view this post on Zulip Markus Himmel (Aug 03 2020 at 15:30):

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

view this post on Zulip Kevin Buzzard (Aug 03 2020 at 15:31):

How about card = 1?

view this post on Zulip Mario Carneiro (Aug 03 2020 at 15:32):

I assume that's one of the two mentioned uses

view this post on Zulip 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