Library ▹ Essentials ▹ Functions
Definition 1.5.18.  Let X, Y be sets, f : X → Y be a function. We define:
f is bijective  :⇔  f is injective and f is surjective  ⇔  ∀ y ∈ Y : ∃! x ∈ X : f(x) = y  ⇔  ∃ g : Y → X : [g ∘ f = idX and f ∘ g = idY]  ⇔  ∃! g : Y → X : [g ∘ f = idX and f ∘ g = idY]
Equivalence.  No proof.
References.
  • https://en.wikipedia.org/wiki/Bijective_function
  • https://mathworld.wolfram.com/Bijection.html
  • https://proofwiki.org/wiki/Definition:Bijection
  • https://proofwiki.org/wiki/Bijection_iff_Left_and_Right_Inverse
  • https://ncatlab.org/nlab/show/bijection
  • https://leanprover-community.github.io/mathlib_docs/init/function.html#function.bijective
  • https://leanprover-community.github.io/mathlib_docs/logic/function/basic.html#function.bijective_iff_has_inverse
[View Source]