equal
deleted
inserted
replaced
6 -- Composition of relations, the identity relation |
6 -- Composition of relations, the identity relation |
7 -- Injections, surjections, bijections |
7 -- Injections, surjections, bijections |
8 -- Lemmas for the Schroeder-Bernstein Theorem |
8 -- Lemmas for the Schroeder-Bernstein Theorem |
9 *) |
9 *) |
10 |
10 |
11 header{*Injections, Surjections, Bijections, Composition*} |
11 section{*Injections, Surjections, Bijections, Composition*} |
12 |
12 |
13 theory Perm imports func begin |
13 theory Perm imports func begin |
14 |
14 |
15 definition |
15 definition |
16 (*composition of relations and functions; NOT Suppes's relative product*) |
16 (*composition of relations and functions; NOT Suppes's relative product*) |