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
=
id
X
and
f
∘
g
=
id
Y
]
⇔
∃!
g
:
Y
→
X
: [
g
∘
f
=
id
X
and
f
∘
g
=
id
Y
]
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