library/subfinite.tex


1
2
3
4
5
6
7
8
9
10
11
12

\import{function.tex}
\import{nat.tex}

\begin{definition}\label{subfinite}
    $X$ is subfinite iff
        there exists a natural number $k$ such that
        there exists an injective function $f$ from $k$ to $X$.
\end{definition}

\begin{proposition}\label{emptyset_subfinite}
    $\emptyset$ is subfinite.
\end{proposition}