Zulip Chat Archive

Stream: new members

Topic: Injective under exists


view this post on Zulip Yakov Pechersky (Oct 15 2020 at 21:09):

Is there the equivalent of this statement, that one can apply an injective function under an existential? Maybe somewhere in pi?

example {α β γ : Type*} {y : β} {f : α  β} {g : β  γ} (g_inj : function.injective g)
  (h :  x, g (f x) = g y) :  x, f x = y :=
exists.elim h (λ x H, exists.intro x (g_inj H))

view this post on Zulip Mario Carneiro (Oct 15 2020 at 21:10):

That looks like exists.imp g_inj

view this post on Zulip Mario Carneiro (Oct 15 2020 at 21:11):

example {α β γ : Type*} {y : β} {f : α  β} {g : β  γ} (g_inj : function.injective g)
  (h :  x, g (f x) = g y) :  x, f x = y := h.imp (λ _ H, g_inj H)

view this post on Zulip Yakov Pechersky (Oct 15 2020 at 21:12):

Great, thanks!


Last updated: May 08 2021 at 04:14 UTC