'a,'b:S, P:('b
), rep:('a'b), abs:('b'a).
Thm* iso_pair('a;'b;P;rep;abs)
Thm*
Thm* (
a:'a. abs(rep(a)) = a) & (r:'b. P(r) = ((rep(abs(r))) =
r))P:('aType), x:'a. P(x) (y:'a. P(y) x = y) (@y:'a. P(y)) = x| Theorem | Name |
| 'a,'b:S, P:('b), rep:('a'b), abs:('b'a).
Thm* iso_pair('a;'b;P;rep;abs) Thm*
Thm* ( a:'a. abs(rep(a)) = a) & (r:'b. P(r) = ((rep(abs(r))) = r)) | [iso_pair_char] |
| cites the following: | |
| P:('aType), x:'a. P(x) (y:'a. P(y) x = y) (@y:'a. P(y)) = x | [choose_unique] |