exists_unique from equiv

Stream: Is there code for X?

[Eric Wieser]

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]

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)⟩

[Mario Carneiro]

LGTM

[Eric Wieser]

Should probably be an iff, right?

[Mario Carneiro]

I suppose it could be

[Mario Carneiro]

f should be implicit

[Mario Carneiro]

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

[Mario Carneiro]

probably still good to have the theorem though

[Eric Wieser]

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]

Are those names in the right order?

[Patrick Massot]

Are you sure those lemmas are not there yet?

[Eric Wieser]

#5995

[Eric Wieser]

No, I'm not sure

[Eric Wieser]

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

[Mario Carneiro]

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

[Mario Carneiro]

The iff lemma should be function.bijective_iff_exists_unique without the dot

[Eric Wieser]

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