Composition


THEOREM    Composite of injections is injection.

Proof available

THEOREM    Composite of surjections is surjection.

Proof available

THEOREM    Composite of bijections is bijection.

Proof available

THEOREM    Function composition is associative
Fun.comp_assoc: ?f \(\circ\) ?g \(\circ\) ?h = ?f \(\circ\) (?g \(\circ\) ?h)

Proof unavailable