| changeset 2469 | b50b8c0eec01 |
| parent 1478 | 2b8c2a7547ab |
| child 13168 | afcbca3498b0 |
| 2468:428efffe8599 | 2469:b50b8c0eec01 |
|---|---|
4 Copyright 1994 University of Cambridge |
4 Copyright 1994 University of Cambridge |
5 |
5 |
6 Relations in Zermelo-Fraenkel Set Theory |
6 Relations in Zermelo-Fraenkel Set Theory |
7 *) |
7 *) |
8 |
8 |
9 Rel = ZF + |
9 Rel = domrange + |
10 consts |
10 consts |
11 refl,irrefl,equiv :: [i,i]=>o |
11 refl,irrefl,equiv :: [i,i]=>o |
12 sym,asym,antisym,trans :: i=>o |
12 sym,asym,antisym,trans :: i=>o |
13 trans_on :: [i,i]=>o ("trans[_]'(_')") |
13 trans_on :: [i,i]=>o ("trans[_]'(_')") |
14 |
14 |