equal
deleted
inserted
replaced
39 h :: "'a*'b => 'c" (*isomorphism between 'a * 'b and 'c *) |
39 h :: "'a*'b => 'c" (*isomorphism between 'a * 'b and 'c *) |
40 slice :: ['c set, 'b] => 'a set |
40 slice :: ['c set, 'b] => 'a set |
41 f_act :: "('c * 'c) set => ('a*'a) set" |
41 f_act :: "('c * 'c) set => ('a*'a) set" |
42 |
42 |
43 assumes |
43 assumes |
44 inj_h "inj h" |
44 bij_h "bij h" |
45 surj_h "surj h" |
|
46 defines |
45 defines |
47 f_def "f z == fst (inv h z)" |
46 f_def "f z == fst (inv h z)" |
48 g_def "g z == snd (inv h z)" |
47 g_def "g z == snd (inv h z)" |
49 slice_def "slice Z y == {x. h(x,y) : Z}" |
48 slice_def "slice Z y == {x. h(x,y) : Z}" |
50 f_act_def "f_act act == (%(z,z'). (f z, f z')) `` act" |
49 f_act_def "f_act act == (%(z,z'). (f z, f z')) `` act" |