37 id :: 'a => 'a |
37 id :: 'a => 'a |
38 "id == %x. x" |
38 "id == %x. x" |
39 |
39 |
40 o :: ['b => 'c, 'a => 'b, 'a] => 'c (infixl 55) |
40 o :: ['b => 'c, 'a => 'b, 'a] => 'c (infixl 55) |
41 "f o g == %x. f(g(x))" |
41 "f o g == %x. f(g(x))" |
|
42 |
|
43 inv :: ('a => 'b) => ('b => 'a) |
|
44 "inv(f::'a=>'b) == % y. @x. f(x)=y" |
42 |
45 |
43 inj_on :: ['a => 'b, 'a set] => bool |
46 inj_on :: ['a => 'b, 'a set] => bool |
44 "inj_on f A == ! x:A. ! y:A. f(x)=f(y) --> x=y" |
47 "inj_on f A == ! x:A. ! y:A. f(x)=f(y) --> x=y" |
45 |
|
46 surj :: ('a => 'b) => bool (*surjective*) |
|
47 "surj f == ! y. ? x. y=f(x)" |
|
48 |
|
49 inv :: ('a => 'b) => ('b => 'a) |
|
50 "inv(f::'a=>'b) == % y. @x. f(x)=y" |
|
51 |
|
52 |
|
53 |
48 |
54 syntax |
49 syntax |
55 inj :: ('a => 'b) => bool (*injective*) |
50 inj :: ('a => 'b) => bool (*injective*) |
56 |
51 |
57 translations |
52 translations |
58 "inj f" == "inj_on f UNIV" |
53 "inj f" == "inj_on f UNIV" |
|
54 |
|
55 constdefs |
|
56 surj :: ('a => 'b) => bool (*surjective*) |
|
57 "surj f == ! y. ? x. y=f(x)" |
|
58 |
|
59 bij :: ('a => 'b) => bool (*bijective*) |
|
60 "bij f == inj f & surj f" |
|
61 |
59 |
62 |
60 (*The Pi-operator, by Florian Kammueller*) |
63 (*The Pi-operator, by Florian Kammueller*) |
61 |
64 |
62 constdefs |
65 constdefs |
63 Pi :: "['a set, 'a => 'b set] => ('a => 'b) set" |
66 Pi :: "['a set, 'a => 'b set] => ('a => 'b) set" |