Zulip Chat Archive

Stream: general

Topic: equiv_subsingleton


view this post on Zulip Johan Commelin (Jan 14 2019 at 14:06):

I couldn't find this in mathlib. Is this considered useful enough to include?

lemma equiv_subsingleton {α β : Type*} [subsingleton α] [subsingleton β] (f : α  β) (g : β  α) :
α  β :=
{ to_fun := f,
  inv_fun := g,
  left_inv := λ _, subsingleton.elim _ _,
  right_inv := λ _, subsingleton.elim _ _, }

If so, where should it go?

view this post on Zulip Chris Hughes (Jan 14 2019 at 14:10):

Only one of them needs to be a subsingleton.

view this post on Zulip Chris Hughes (Jan 14 2019 at 14:27):

I misread the statement

view this post on Zulip Kenny Lau (Jan 14 2019 at 21:13):

@Johan Commelin it isn't a lemma

view this post on Zulip Reid Barton (Jan 15 2019 at 05:46):

Yes it is useful. Not sure about the name though, it should be in the equiv namespace. Perhaps equiv.of_subsingleton?


Last updated: May 13 2021 at 19:20 UTC