Definition num_lt_equi

Definition. num_lt_equi
num_lt X Y ↔ num_le X Y ∧ ¬∃f. sur f X Y

A set X is called strictly smaller than Y, written |X| < |Y|, if X is not greater than Y and there is no surjection from X to Y.