Stream: Is there code for X?

Topic: Left and right inverse of function

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.

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