f:(
a
2).
Thm* (
i:a. P(i) 
f(i) = 1 
2) 
({x:a| P(x) } ~ (Msize(f)))a:, b:(a). (i:a
b(i)) ~ (
i:a. b(i))| Rank | Theorem | Name |
| 8 | f:(a2).
Thm* ( i:a. P(i) f(i) = 1 2) ({x:a| P(x) } ~ (Msize(f))) | [card_st_vs_msize] |
| cites the following: | ||
| 7 | a:, b:(a). (i:ab(i)) ~ ( i:a. b(i)) | [card_sigma_vs_nsub_sigma] |