## Stream: new members

### Topic: bijection iff of an equiv

#### Yakov Pechersky (Jan 10 2021 at 10:31):

Is there a lemma like this?

lemma equiv_inv_iff {α β : Type*} (e : α ≃ β) {a : α} {b : β} :
e a = b ↔ a = e.symm b :=
begin
sorry
end


#### Patrick Massot (Jan 10 2021 at 10:32):

library_search

Last updated: May 12 2021 at 23:13 UTC