## Stream: Is there code for X?

### Topic: exists_unique from equiv

#### Eric Wieser (Feb 01 2021 at 11:53):

import data.equiv.basic

lemma equiv.exists_unique {α β : Type*} (e : α ≃ β) (b : β) : ∃! (a : α), e a = b :=
-- by library_search  fails
⟨e.symm b, e.apply_symm_apply _, λ a h, e.eq_symm_apply.mpr h⟩


#### Eric Wieser (Feb 01 2021 at 12:01):

Or perhaps even

lemma function.bijective.exists_unique {α β : Type*} (f : α → β) (hf : function.bijective f) (b : β) :
∃! (a : α), f a = b :=
let ⟨a, ha⟩ := hf.2 b in ⟨a, ha, λ a' ha', hf.1 (ha'.trans ha.symm)⟩


LGTM

#### Eric Wieser (Feb 01 2021 at 12:07):

Should probably be an iff, right?

#### Mario Carneiro (Feb 01 2021 at 12:07):

I suppose it could be

#### Mario Carneiro (Feb 01 2021 at 12:07):

f should be implicit

#### Mario Carneiro (Feb 01 2021 at 12:08):

Ah, actually you won't get projection notation with the iff version

#### Mario Carneiro (Feb 01 2021 at 12:08):

probably still good to have the theorem though

#### Eric Wieser (Feb 01 2021 at 12:11):

lemma function.bijective.iff_exists_unique {α β : Sort*} (f : α → β) : function.bijective f ↔
∀ b : β, ∃! (a : α), f a = b :=
⟨ λ hf b, let ⟨a, ha⟩ := hf.2 b in ⟨a, ha, λ a' ha', hf.1 (ha'.trans ha.symm)⟩,
λ he, ⟨
λ a a' h, let ⟨a'', _, ha''⟩ := he (f a) in (ha'' a rfl).trans (ha'' a' h.symm).symm,
λ b, let ⟨a, ha, _⟩ := he b in ⟨a, ha⟩ ⟩⟩

lemma function.bijective.exists_unique {α β : Sort*} {f : α → β} (hf : function.bijective f) (b : β) :
∃! (a : α), f a = b :=
(function.bijective.iff_exists_unique f).mp hf b


#### Eric Wieser (Feb 01 2021 at 12:14):

Are those names in the right order?

#### Patrick Massot (Feb 01 2021 at 12:26):

Are you sure those lemmas are not there yet?

#5995

No, I'm not sure

#### Eric Wieser (Feb 01 2021 at 12:27):

But they're not in logic.function.basic where I'd expect to find them

#### Mario Carneiro (Feb 01 2021 at 12:34):

I am not too surprised that they aren't there; exists_unique doesn't have many lemmas about it

#### Mario Carneiro (Feb 01 2021 at 12:35):

The iff lemma should be function.bijective_iff_exists_unique without the dot

#### Eric Wieser (Feb 01 2021 at 12:36):

Updated in the PR. I was able to golf the reverse direction a bit using existing lemmas too

Last updated: May 17 2021 at 16:26 UTC