equal
deleted
inserted
replaced
30 INTER1 :: ['a => 'b set] => 'b set (binder "INT " 10) |
30 INTER1 :: ['a => 'b set] => 'b set (binder "INT " 10) |
31 Union, Inter :: (('a set) set) => 'a set (*of a set*) |
31 Union, Inter :: (('a set) set) => 'a set (*of a set*) |
32 Pow :: 'a set => 'a set set (*powerset*) |
32 Pow :: 'a set => 'a set set (*powerset*) |
33 range :: ('a => 'b) => 'b set (*of function*) |
33 range :: ('a => 'b) => 'b set (*of function*) |
34 Ball, Bex :: ['a set, 'a => bool] => bool (*bounded quantifiers*) |
34 Ball, Bex :: ['a set, 'a => bool] => bool (*bounded quantifiers*) |
35 inj, surj :: ('a => 'b) => bool (*inj/surjective*) |
|
36 inj_onto :: ['a => 'b, 'a set] => bool |
|
37 "``" :: ['a => 'b, 'a set] => ('b set) (infixr 90) |
35 "``" :: ['a => 'b, 'a set] => ('b set) (infixr 90) |
38 (*membership*) |
36 (*membership*) |
39 "op :" :: ['a, 'a set] => bool ("(_/ : _)" [50, 51] 50) |
37 "op :" :: ['a, 'a set] => bool ("(_/ : _)" [50, 51] 50) |
40 |
38 |
41 |
39 |
147 Union_def "Union S == (UN x:S. x)" |
145 Union_def "Union S == (UN x:S. x)" |
148 Pow_def "Pow A == {B. B <= A}" |
146 Pow_def "Pow A == {B. B <= A}" |
149 empty_def "{} == {x. False}" |
147 empty_def "{} == {x. False}" |
150 insert_def "insert a B == {x.x=a} Un B" |
148 insert_def "insert a B == {x.x=a} Un B" |
151 image_def "f``A == {y. ? x:A. y=f(x)}" |
149 image_def "f``A == {y. ? x:A. y=f(x)}" |
152 inj_def "inj f == ! x y. f(x)=f(y) --> x=y" |
|
153 inj_onto_def "inj_onto f A == ! x:A. ! y:A. f(x)=f(y) --> x=y" |
|
154 surj_def "surj f == ! y. ? x. y=f(x)" |
|
155 |
150 |
156 end |
151 end |
157 |
152 |
158 |
153 |
159 ML |
154 ML |