Definition num_le_equi
Definition.
num_le_equi
num_le X Y ↔ ∃f. inj f X Y
A set X is called
not greater than
Y, written |X| ≤ |Y|, if there exists an
injection
from X to Y.