## Stream: Is there code for X?

### Topic: unique from empty

#### Yakov Pechersky (Feb 17 2021 at 19:55):

Do we have something that can give:

example : option (fin 0) ≃ unit := sorry


Something like pi.unique_of_empty but saying that unique [option α] when α ≃ empty.

#### Floris van Doorn (Feb 17 2021 at 20:10):

I guess you already know about docs#equiv_punit_of_unique? The other part seems like it's missing, but is very easy.

#### Mario Carneiro (Feb 17 2021 at 20:12):

the other direction sounds like the composition of two lemmas, equivs preserve unique and unique pempty

#### Mario Carneiro (Feb 17 2021 at 20:13):

I wouldn't make that into one lemma unless it's one half of an iff statement

#### Floris van Doorn (Feb 17 2021 at 20:13):

I think (\a -> false) -> unique (option \a) is a reasonable lemma to have.

#### Mario Carneiro (Feb 17 2021 at 20:14):

that could also be one half of an iff statement

#### Floris van Doorn (Feb 17 2021 at 20:14):

Honestly, I feel like we should add [is_empty \a] as a typeclass

I'm a fan

#### Mario Carneiro (Feb 17 2021 at 20:14):

that works for me

#### Mario Carneiro (Feb 17 2021 at 20:15):

there aren't that many instances but there are at least 2 or 3

#### Johan Commelin (Feb 17 2021 at 20:15):

We already have subsingleton, unique, nonempty and nontrivial. It's only reasonable to also have is_empty.

#### Mario Carneiro (Feb 17 2021 at 20:16):

Of course you have to keep in mind that because of the @[class] def thing this might not be easier to use than A -> false

#### Johan Commelin (Feb 17 2021 at 20:16):

empty, pempty, {x // x \in \empty}, false, prime_spectrum punit

#### Mario Carneiro (Feb 17 2021 at 20:16):

fin 0, A -> false where nonempty A

#### Floris van Doorn (Feb 17 2021 at 20:17):

↥∅ for ∅ in various types

#### Floris van Doorn (Feb 17 2021 at 20:17):

Mario Carneiro said:

A -> false where nonempty A

A -> Bwhere nonempty A and is_empty B :)

#### Johan Commelin (Feb 17 2021 at 20:17):

I think we have convincingly, and even constructively! proven Marios conjecture that there are at least 2 or 3 examples (-;

#### Mario Carneiro (Feb 17 2021 at 20:17):

lean has too many ways to say nothing :)

#### Johan Commelin (Feb 17 2021 at 20:18):

It's a hard problem! If you can fix it, I guess you solved the "canonical isomorphism" problem (-;

#### Gabriel Ebner (Feb 17 2021 at 20:18):

Floris van Doorn said:

Mario Carneiro said:

A -> false where nonempty A

A -> Bwhere nonempty A and is_empty B :)

I think you can drop the nonempty A assumption here.

I don't think so

#### Mario Carneiro (Feb 17 2021 at 20:18):

false -> false is true

#### Gabriel Ebner (Feb 17 2021 at 20:18):

Oops. You're right of course.

#### Johan Commelin (Feb 17 2021 at 20:19):

If we introduce this class, there will be 37 files (or more) where we can replace (p)empty using this class.

#### Mario Carneiro (Feb 17 2021 at 20:20):

not all of those would necessarily be a good idea

#### Mario Carneiro (Feb 17 2021 at 20:20):

in particular we don't want algebraic classes for these types just because they are empty

#### Johan Commelin (Feb 17 2021 at 20:21):

Sure, but we prove things about mv_polynomial pempty R and also about mv_polynomial (fin 0) R

#### Mario Carneiro (Feb 17 2021 at 20:23):

certainly if be have any duplicated lemmas then that's a good candidate, but if you want the initial object of Set to inhabit a typeclass you probably don't want that to be generic

#### Mario Carneiro (Feb 17 2021 at 20:25):

docs#equiv.prod_empty looks like it could be generalized, although prod_punit isn't

#### Kevin Buzzard (Feb 17 2021 at 20:36):

When I was proving some instances of free_abelian_group I proved free_abelian_group pempty ≃+ unit and free_abelian_group punit ≃+ ℤ and then in the PR process Eric said I would be better off proving punit_equiv (T : Type*) [unique T] : free_abelian_group T ≃+ ℤ and pempty_unique : unique (free_abelian_group pempty). This does seem like a natural extension of this. The argument the other way is of course xkcd#927

#### Gabriel Ebner (Feb 17 2021 at 21:34):

Another lemma that would benefit from this type class:

lemma is_basis_empty [subsingleton M] (h_empty : ¬ nonempty ι) : is_basis R (λ x : ι, (0 : M)) :=


#### Eric Wieser (Feb 17 2021 at 21:36):

docs#is_basis_empty isn't yet stated exactly like that, but will be soon ;)

#### Mario Carneiro (Feb 17 2021 at 21:38):

oh, I spent a while looking at docs#is_basis_empty_bot trying to figure out why it's not a straight generalization of the lemma before it

#### Eric Wieser (Feb 17 2021 at 21:40):

Yeah, I have a PR that removes it

#6281

#### Mario Carneiro (Feb 17 2021 at 21:55):

No I mean a generalization in the other direction

#### Mario Carneiro (Feb 17 2021 at 21:56):

if you look at the two statements in docgen the only difference is that the _bot lemma has one fewer assumption

#### Eric Wieser (Feb 17 2021 at 22:52):

Yes, and it's proved in terms of the other lemma, so I don't understand what you're disagreeing with. Perhaps best to discuss in the PR.

#### Yury G. Kudryashov (Mar 02 2021 at 05:16):

We also have some lemmas about supr/infi over an empty type and filters on an empty type.

#### Eric Wieser (Mar 02 2021 at 07:14):

My impression is that now we're just waiting for someone to make the PR

#### Floris van Doorn (May 13 2021 at 05:31):

I've started this on branch#is_empty.

#### Yakov Pechersky (May 13 2021 at 05:45):

Awesome! (Bikeshedding comment) It's unfortunate that empty is taken, because now is_empty doesn't agree with nonempty

Last updated: May 16 2021 at 05:21 UTC