| changeset 20326 | cbf31171c147 |
| parent 19064 | bf19cc5a7899 |
| child 31723 | f5cafe803b55 |
| 20325:ec52000deb44 | 20326:cbf31171c147 |
|---|---|
18 .. |
18 .. |
19 qed |
19 qed |
20 |
20 |
21 consts |
21 consts |
22 ONE_ONE :: "('a => 'b) => bool" |
22 ONE_ONE :: "('a => 'b) => bool" |
23 ONTO :: "('a => 'b) => bool" |
|
24 |
23 |
25 defs |
24 defs |
26 ONE_ONE_DEF: "ONE_ONE f == ALL x y. f x = f y --> x = y" |
25 ONE_ONE_DEF: "ONE_ONE f == ALL x y. f x = f y --> x = y" |
27 |
26 |
28 lemma ONE_ONE_rew: "ONE_ONE f = inj_on f UNIV" |
27 lemma ONE_ONE_rew: "ONE_ONE f = inj_on f UNIV" |