Zulip Chat Archive

Stream: new members

Topic: inverse of injective functions


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

view this post on Zulip Mario Carneiro (May 08 2019 at 10:23):

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

view this post on Zulip Mario Carneiro (May 08 2019 at 10:24):

alternatively, this seems like a good lemma on its own

view this post on Zulip Mario Carneiro (May 08 2019 at 10:26):

this is some kind of categorical thing about split monos

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