30 range :: ('a => 'b) => 'b set (*of function*) |
30 range :: ('a => 'b) => 'b set (*of function*) |
31 Ball, Bex :: ['a set, 'a => bool] => bool (*bounded quantifiers*) |
31 Ball, Bex :: ['a set, 'a => bool] => bool (*bounded quantifiers*) |
32 inj, surj :: ('a => 'b) => bool (*inj/surjective*) |
32 inj, surj :: ('a => 'b) => bool (*inj/surjective*) |
33 inj_onto :: ['a => 'b, 'a set] => bool |
33 inj_onto :: ['a => 'b, 'a set] => bool |
34 "``" :: ['a => 'b, 'a set] => ('b set) (infixr 90) |
34 "``" :: ['a => 'b, 'a set] => ('b set) (infixr 90) |
35 ":" :: ['a, 'a set] => bool (infixl 50) (*membership*) |
35 (*membership*) |
|
36 "op :" :: ['a, 'a set] => bool ("(_/ : _)" [50,51] 50) |
36 |
37 |
37 |
38 |
38 syntax |
39 syntax |
39 |
40 |
40 UNIV :: 'a set |
41 UNIV :: 'a set |
41 |
42 |
42 "~:" :: ['a, 'a set] => bool (infixl 50) |
43 (*infix synatx for non-membership*) |
|
44 "op ~:" :: ['a, 'a set] => bool ("(_/ ~: _)" [50,51] 50) |
43 |
45 |
44 "@Finset" :: args => 'a set ("{(_)}") |
46 "@Finset" :: args => 'a set ("{(_)}") |
45 |
47 |
46 "@Coll" :: [pttrn, bool] => 'a set ("(1{_./ _})") |
48 "@Coll" :: [pttrn, bool] => 'a set ("(1{_./ _})") |
47 "@SetCompr" :: ['a, idts, bool] => 'a set ("(1{_ |/_./ _})") |
49 "@SetCompr" :: ['a, idts, bool] => 'a set ("(1{_ |/_./ _})") |