Zulip Chat Archive

Stream: Is there code for X?

Topic: Left and right inverse of function

view this post on Zulip Pedro Minicz (Aug 11 2020 at 23:30):

Is there a definition like the following in mathlib?

variables {α : Type*} {β : Type*}

def inverse (g : β  α) (f : α  β) : Prop :=
  function.left_inverse g f  function.right_inverse g f

I believe there should be one in logic.function.basic, but I can't it.

view this post on Zulip Adam Topaz (Aug 12 2020 at 00:50):

You can probably get what you need with docs#equiv

Last updated: May 07 2021 at 21:10 UTC