## Stream: new members

### Topic: inverse of injective functions

#### Alexander Bentkamp (May 08 2019 at 10:21):

Given a function g : α → ɣ and an injective function f : β → ɣ, such that g.range ⊆ f.range, how can I access the function f⁻¹ ∘ g : α → β in Lean?

#### Mario Carneiro (May 08 2019 at 10:23):

there might be an equiv B ~= f.range in equiv.basic?

#### Mario Carneiro (May 08 2019 at 10:24):

alternatively, this seems like a good lemma on its own

#### Mario Carneiro (May 08 2019 at 10:26):

this is some kind of categorical thing about split monos

#### Alexander Bentkamp (May 08 2019 at 10:31):

Yes: equiv.set.range. That should do it. Thanks!

Last updated: May 08 2021 at 09:11 UTC