Injection


Definition

Fun.inj_def: inj ?f = (\(\forall\)x y. ?f x = ?f y \(\longrightarrow\) x = y)
THEOREM    The composition of two injective functions is injective.

Proof available

Proper subsets