Library ▹ Essentials ▹ Functions
Definition 1.5.29.  Let X, Y be sets, f : X ↔ Y be a bijection. For g : Y ↔ X, we define:
f-1 = g  :⇔  g ∘ f = idX  ⇔  f ∘ g = idY
Equivalence.  No proof.
Well-definedness.  No proof.
References.
  • https://en.wikipedia.org/wiki/Inverse_function
  • https://mathworld.wolfram.com/InverseFunction.html
  • https://proofwiki.org/wiki/Definition:Inverse_Mapping
  • https://ncatlab.org/nlab/show/inverse
  • https://leanprover-community.github.io/mathlib_docs/logic/function/basic.html#function.inv_fun
[View Source]