## Stream: new members

### Topic: Injective under exists

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


#### Mario Carneiro (Oct 15 2020 at 21:10):

That looks like exists.imp g_inj

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


#### Yakov Pechersky (Oct 15 2020 at 21:12):

Great, thanks!

Last updated: May 08 2021 at 04:14 UTC