equal
deleted
inserted
replaced
26 Lift :: "i set => i set" ("(3[_])") |
26 Lift :: "i set => i set" ("(3[_])") |
27 |
27 |
28 SPLIT :: "[i, [i, i] => i set] => i set" |
28 SPLIT :: "[i, [i, i] => i set] => i set" |
29 |
29 |
30 "@Pi" :: "[idt, i set, i set] => i set" ("(3PROD _:_./ _)" |
30 "@Pi" :: "[idt, i set, i set] => i set" ("(3PROD _:_./ _)" |
31 [0,0,60] 60) |
31 [0,0,60] 60) |
32 |
32 |
33 "@Sigma" :: "[idt, i set, i set] => i set" ("(3SUM _:_./ _)" |
33 "@Sigma" :: "[idt, i set, i set] => i set" ("(3SUM _:_./ _)" |
34 [0,0,60] 60) |
34 [0,0,60] 60) |
35 |
35 |
36 "@->" :: "[i set, i set] => i set" ("(_ ->/ _)" [54, 53] 53) |
36 "@->" :: "[i set, i set] => i set" ("(_ ->/ _)" [54, 53] 53) |
37 "@*" :: "[i set, i set] => i set" ("(_ */ _)" [56, 55] 55) |
37 "@*" :: "[i set, i set] => i set" ("(_ */ _)" [56, 55] 55) |
38 "@Subtype" :: "[idt, 'a set, o] => 'a set" ("(1{_: _ ./ _})") |
38 "@Subtype" :: "[idt, 'a set, o] => 'a set" ("(1{_: _ ./ _})") |
39 |
39 |