Bijective function

Set

context $X,Y$ … set
definiendum $ f\in \mathrm{Bijective}(X,Y) $
inclusion $ f\in \mathrm{Injective}(X,Y) $
inclusion $ f\in \mathrm{Surjective}(X,Y) $

Discussion

Predicates

predicate $X\approx Y\equiv \mathrm{Bijective}(X,Y)\ne\emptyset$

We also write $X$ equinumerous $Y$.

predicate $X\preccurlyeq Y \equiv \exists (X'\subseteq Y).\ X'\approx X$

We also write $X$ smaller $Y$.

predicate $Y$ … countably infinite $\equiv \mathbb N\approx Y$

Parents

Context

Injective function, Surjective function