bijection iff of an equiv

Stream: new members

[Yakov Pechersky]

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]

library_search