Definition bij_equi
Definition.
bij_equi
bij f X Y ↔ inj f X Y ∧ sur f X Y
A
mapping
f from X to Y is called
bijective
if it is
injective
as well as
surjective
.