equal
deleted
inserted
replaced
6 Relations in Zermelo-Fraenkel Set Theory |
6 Relations in Zermelo-Fraenkel Set Theory |
7 *) |
7 *) |
8 |
8 |
9 Rel = equalities + |
9 Rel = equalities + |
10 consts |
10 consts |
11 refl,irrefl,equiv :: [i,i]=>o |
11 refl :: "[i,i]=>o" |
12 sym,asym,antisym,trans :: i=>o |
12 irrefl :: "[i,i]=>o" |
13 trans_on :: [i,i]=>o ("trans[_]'(_')") |
13 equiv :: "[i,i]=>o" |
|
14 sym :: "i=>o" |
|
15 asym :: "i=>o" |
|
16 antisym :: "i=>o" |
|
17 trans :: "i=>o" |
|
18 trans_on :: "[i,i]=>o" ("trans[_]'(_')") |
14 |
19 |
15 defs |
20 defs |
16 refl_def "refl(A,r) == (ALL x: A. <x,x> : r)" |
21 refl_def "refl(A,r) == (ALL x: A. <x,x> : r)" |
17 |
22 |
18 irrefl_def "irrefl(A,r) == ALL x: A. <x,x> ~: r" |
23 irrefl_def "irrefl(A,r) == ALL x: A. <x,x> ~: r" |