Zulip Chat Archive

Stream: Is there code for X?

Topic: exists_unique from equiv


view this post on Zulip 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

view this post on Zulip 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)⟩

view this post on Zulip Mario Carneiro (Feb 01 2021 at 12:06):

LGTM

view this post on Zulip Eric Wieser (Feb 01 2021 at 12:07):

Should probably be an iff, right?

view this post on Zulip Mario Carneiro (Feb 01 2021 at 12:07):

I suppose it could be

view this post on Zulip Mario Carneiro (Feb 01 2021 at 12:07):

f should be implicit

view this post on Zulip Mario Carneiro (Feb 01 2021 at 12:08):

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

view this post on Zulip Mario Carneiro (Feb 01 2021 at 12:08):

probably still good to have the theorem though

view this post on Zulip 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

view this post on Zulip Eric Wieser (Feb 01 2021 at 12:14):

Are those names in the right order?

view this post on Zulip Patrick Massot (Feb 01 2021 at 12:26):

Are you sure those lemmas are not there yet?

view this post on Zulip Eric Wieser (Feb 01 2021 at 12:27):

#5995

view this post on Zulip Eric Wieser (Feb 01 2021 at 12:27):

No, I'm not sure

view this post on Zulip Eric Wieser (Feb 01 2021 at 12:27):

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

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Feb 01 2021 at 12:35):

The iff lemma should be function.bijective_iff_exists_unique without the dot

view this post on Zulip 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