equiv_subsingleton

Stream: general

[Johan Commelin]

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?

[Chris Hughes]

Only one of them needs to be a subsingleton.

[Chris Hughes]

I misread the statement

[Kenny Lau]

@Johan Commelin it isn't a lemma

[Reid Barton]

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